IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
8
Thm*
m
,
k
:
.
k
<
m
k
!
m
= 0
[factorial_tail_via_iter_zero]
cites the following:
7
Thm*
(
i
:{
a
..
b
}.
e
(
i
) = 0)
(
i
:{
a
..
b
}.
e
(
i
)) = 0
[zero_ann_iter_via_intseg]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops
Sections
DiscrMathExt
Doc
m,k:
. k<m 
k!m = 0 
i:{a..b
}. e(i) = 0) (
i:{a..b}. e(i)) = 0m,k:. k<m k!m = 0 i:{a..b}. e(i) = 0) ( i:{a..b}. e(i)) = 0