(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
1.
T
: Type
2.
F
:
k
:
. (
k
T
)
(
k
+1)
T
n
:
. Y(
F
)
n
T
By:
NatInd Concl
Generated subgoals:
1
Y(
F
)
0
T
PREMISE
2
3.
n
:
4. 0<
n
5. Y(
F
)
(
n
-1)
T
Y(
F
)
n
T
4
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
n:. Y(F) 
nTk:. (kT)(k+1)T
n:. Y(F) nT Y(F) 0T
(n-1)T
Y(F) nT
