Nuprl - Proof: qadd functionality 1 1 1 1 1

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

1. p1 :

2. p2 :

3. q1 :

4. q2 :

5. r1 :

6. r2 :

7. s1 :

8. s2 :

9. p1

q2 = q1

p2
10. r1

s2 = s1

(p1

r2+r1

p2)

s2 = (q1

s2+s1

q2)

By:	(Using [`n',(r2s2)] (FwdThru Thm* a,b,n:. a = b na = nb [9])) THEN (Using [`n',(p2q2)] (FwdThru Thm* a,b,n:. a = b na = nb [10]))

Generated subgoal:

1 11. r2s2p1q2 = r2s2q1p2
12. p2q2r1s2 = p2q2s1r2
(p1r2+r1p2)q2s2 = (q1s2+s1q2)p2r2
1 step

About:

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