(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
factorial
tail
via
iter
null
1
1.
m
:
2.
k
:
3.
m
= 0
(
i
:{
k
-
m
..
k
}.
i
+1) = 1
By:
BackThru:
Thm*
f
:(
A
A
A
),
u
:
A
,
a
,
b
:
,
e
:({
a
..
b
}
A
).
Thm*
b
a
(Iter(
f
;
u
)
i
:{
a
..
b
}.
e
(
i
)) =
u
...
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
(2steps total)
PrintForm
Definitions
Lemmas
IteratedBinops
Sections
DiscrMathExt
Doc
(
i:{k-m..k
}. i+1) = 1 
( i:{k-m..k}. i+1) = 1 
f:(A
AA), u:A, a,b:
, e:({a..b}A).
a 
(Iter(f;u) i:{a..b}. e(i)) = u ...
