(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.
T
: Type
2.
F
:
k
:
. (
k
T
)
(
k
+1)
T
Y(
F
)
T
By:
n
:
. Y(
F
)
n
T
Asserted
Generated subgoals:
1
n
:
. Y(
F
)
n
T
6
steps
2
3.
n
:
. Y(
F
)
n
T
Y(
F
)
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
k:
. (k
T)(k+1)T
Y(F) 
Tk:. (kT)(k+1)T
Y(F) T
n:. Y(F) nT Asserted n:. Y(F) nT
n:. Y(F) nT
Y(F) T
