Nuprl - Proof: eq rat trans 1 1 1 1 1 1 1 2

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eq rat trans 1 1 1 1 1 1 1 2

1. x1 :

2. x2 :

3. y1 :

4. y2 :

5. z1 :

6. z2 :

7. x1

y2 = y1

x2
8. y1

z2 = z1

y2
9. x1

z2 = y1

y2
10.

y1 = 0

z2 = z1

By:	Using [`n',(y1y2)] (BackThru Thm* a,b:, n:. na = nb a = b)

Generated subgoals:

1 y1y2 0
1 step

2 y1y2x1z2 = y1y2z1x2
Auto

About:

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