Nuprl - Proof: preserved by star 1 1 2

(8steps total) PrintForm Definitions mb nat Sections MarkB generic Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: preserved by star 1 1 2

1. T : Type
2. P : T

Prop
3. R : T

T

Prop
4.

x,y:T. P(x)

(x R y)

P(y)
5. n :

6. 0<n
7. n-1

0

(

x,y:T. P(x)

(x R^n-1 y)

P(y))
8. n

0
9. x : T
10. y : T
11. P(x)
12. x R^n y

P(y)

By:	MoveToConcl -1 THEN RecUnfold `rel_exp` 0 THEN Reduce 0 THEN SplitOnConclITE THEN Reduce 0

Generated subgoal:

1 12. n = 0
13. z:T. (x R z) & (z R^n-1 y)
P(y)
3 steps

About:

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

(8steps total) PrintForm Definitions mb nat Sections MarkB generic Doc