Nuprl - Proof: qadd functionality 1 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

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

r2
11. r2

q2 = r2

p2
12. p2

s2 = p2

(p1

r2+r1

p2)

s2 = (q1

s2+s1

q2)

By:	FwdThru Thm* i1,i2,j1,j2:. i1 = j1 i2 = j2 i1+i2 = j1+j2 [11;12]

Generated subgoals:

None

About:

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