By: |
((FwdThru ((Thm* a,b,c,x,y:. ((Thm* GCD(a;b;x) ((Thm* ((Thm* GCD(x;c;y) ((Thm* ((Thm* y | a & y | b & y | c & (z:. z | a z | b z | c z | y) (([5;8])) THEN (Simple ((FwdThru ((Thm* a,b,c,x,y:. ((Thm* GCD(a;b;x) ((Thm* ((Thm* GCD(x;c;y) ((Thm* ((Thm* y | a & y | b & y | c & (z:. z | a z | b z | c z | y) (([10;11])) THEN RepD |
1 |
13. y | b 14. y | c 15. z:. z | a z | b z | c z | y 16. z | c 17. z | b 18. z | a 19. z1:. z1 | c z1 | b z1 | a z1 | z y ~ z | 1 step |
About: