Nuprl - Proof: qadd functionality 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. 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/p2 +q r1/r2.num

q1/q2 +q s1/s2.den = q1/q2 +q s1/s2.num

p1/p2 +q r1/r2.den

By:	Unfold `qadd` 0 THEN RW (DepthC qnd_evalC) 0

Generated subgoal:

1 (p1r2+r1p2)q2s2 = (q1s2+s1q2)p2r2
2 steps

About:

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