Nuprl - Proof: rel star finite

(41steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

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

, R:(

Prop), x,y:

n. (x (R^*) y)

(

(n+1). x R^k y)

By:

Auto

Generated subgoals:

1 1. n :
2. R : nnProp
3. x : n
4. y : n
5. x (R^*) y
k:(n+1). x R^k y
39 steps

2 1. n :
2. R : nnProp
3. x : n
4. y : n
5. k:(n+1). x R^k y
x (R^*) y
1 step

About:

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

(41steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc

1	1. n : 2. R : nnProp 3. x : n 4. y : n 5. x (R^*) y k:(n+1). x R^k y	39 steps
2	1. n : 2. R : nnProp 3. x : n 4. y : n 5. k:(n+1). x R^k y x (R^*) y	1 step