Nuprl - Proof: rel star finite 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star finite 1 1 1

1. n :

2. R :

Prop
3. x :

n
4. y :

n
5. n@0 :

. j<n@0

(x R^j y)

(

(n+1). x R^k y)
7. x R^n@0 y

(n+1). x R^k y

By:	Decide (n@0n)

Generated subgoals:

1 8. n@0n
k:(n+1). x R^k y
1 step

2 8. n@0n
k:(n+1). x R^k y
35 steps

About:

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

1	8. n@0n k:(n+1). x R^k y	1 step
2	8. n@0n k:(n+1). x R^k y	35 steps