mb
nat
Sections
MarkB
generic
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Theorem
Name
Thm*
n
:
,
h
,
f
:(
T
T
).
f
^
n
o
h
= primrec(
n
;
h
;
i
,
g
.
f
o
g
)
[fun_exp_compose]
cites the following:
Thm*
n
,
m
:
,
b
:
T
,
c
:(
(
n
+
m
)
T
T
).
Thm*
primrec(
n
+
m
;
b
;
c
) = primrec(
n
;primrec(
m
;
b
;
c
);
i
,
t
.
c
(
i
+
m
,
t
))
[primrec_add]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb
nat
Sections
MarkB
generic
Doc