Nuprl Basics - Proof: sfa doc ycomb typing demo 1 2 1 2 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: sfa doc ycomb typing demo 1 2 1 2 1 1

1. T : Type
2. F :

. (

(k+1)

T
3. n :

4. 0<n
5. Y(F)

(n-1)

T
6. x :

F(Y(F),x)

By:	F (k:. (kT)(k+1)T) Asserted THEN Witness-1: n-1

Generated subgoal:

1 7. F  (k:. (kT)(k+1)T)
8. F  ((n-1)T)(n-1+1)T
  F(Y(F),x)  T
Auto

About:

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