(2steps total)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
division
typing1b
sfa
a
:{...0},
n
:
. (
a
n
)
{...0}
By:
Auto THEN ElaborateDivision Auto 0
Generated subgoal:
1
1.
a
: {...0}
2.
n
:
3.
a
= (
a
n
)
n
+(
a
rem
n
)
4. -(
a
rem
n
)
n
(
a
n
)
0
1
step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
int
2
Sections
StandardLIB
Doc
a:{...0}, n:
. (a 
n) 
{...0} a:{...0}, n:. (a n) {...0}
n)
n+(a rem n)
n
(a n)
0
