Nuprl - Proof: gcd assoc 1

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd assoc 1

1. a :

2. b :

3. c :

gcd(gcd(a;b);c) ~ gcd(a;gcd(b;c))

By:	(FunElim (gcd(a;b) = w)) THEN (FunElim (gcd(b;c) = x)) THEN (FunElim (gcd(w;c) = y)) THEN (FunElim (gcd(a;x) = z))

Generated subgoal:

1 4. w :
5. GCD(a;b;w)
6. x :
7. GCD(b;c;x)
8. y :
9. GCD(w;c;y)
10. z :
11. GCD(a;x;z)
y ~ z
3 steps

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html