(27steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
int
ooc
nat
1
1
a
1
(
i
.if 0
i
i
2 else (-
i
)
2-1 fi)
By:
FunExtensionality
Generated subgoal:
1
1.
x
:
if 0
x
x
2 else (-
x
)
2-1 fi
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(27steps total)
PrintForm
Definitions
Lemmas
DiscreteMath
Sections
DiscrMathExt
Doc
(
i.if 0
i
i
2 else (-i)2-1 fi) 
(i.if 0i i2 else (-i)2-1 fi)
if 0x x2 else (-x)2-1 fi 
