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

(12steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc

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. T : Type
2. F :

k:

. (

k

T)

(k+1)

T
3. n :

4. 0<n
5. Y(F)

(n-1)

T
6. x :

n

Y(F,x)

T

By:	Compute Y(F) * F(Y(F))

Generated subgoal:

1 F(Y(F),x) T
2 steps

About:

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

(12steps total) PrintForm Definitions NuprlPrimitives Sections NuprlLIB Doc