IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
gcd assoc1111 1. a : 2. b : 3. c : 4. w : 5. GCD(a;b;w)
6. x : 7. y : 8. GCD(w;c;y)
9. z : 10. GCD(c;b;x)
11. GCD(x;a;z)
12. y | a 13. y | b 14. y | c 15. z:. z | az | bz | cz | y 16. z | c 17. z | b 18. z | a 19. z1:. z1 | cz1 | bz1 | az1 | z y ~ z
By:
Unfold `assoced` 0 THEN HypBackchain
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html