(6steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ncompose
wf
1
1.
'a
: Type
2.
n
:
3.
x
:
'a
4.
f
:
'a
'a
ncompose(
f
;
n
;
x
)
'a
By:
MoveToConcl 3 THEN NInd 2 THEN StrongAuto
Generated subgoals:
1
2.
f
:
'a
'a
3.
x
:
'a
ncompose(
f
;0;
x
)
'a
2
steps
2
2.
f
:
'a
'a
3.
n
:
4. 0<
n
5.
x
:
'a
. ncompose(
f
;
n
-1;
x
)
'a
6.
x
:
'a
ncompose(
f
;
n
;
x
)
'a
2
steps
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(6steps total)
PrintForm
Definitions
hol
num
Sections
HOLlib
Doc
'a
ncompose(f;n;x) 
'a
'a
ncompose(f;n;x) 'a'a
ncompose(f;0;x) 'a
'a
x:'a. ncompose(f;n-1;x) 'a
ncompose(f;n;x) 'a
