Nuprl - Proof: gcd assoc 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: gcd assoc 1 1

1. a :

2. b :

3. c :

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

By:	(FwdThru Thm* a,b,y:. GCD(a;b;y) GCD(b;a;y) [7]) THEN (FwdThru Thm* a,b,y:. GCD(a;b;y) GCD(b;a;y) [11]) THEN (OnHyps [11;7] Thin)

Generated subgoal:

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

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html