IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm*  f:(AAA), u:A.
Thm*  is_ident(Afu)
Thm*  
Thm*  (a,b:e:({a..b}A).
Thm*  ((i:{a..b}. e(i) = u (Iter(f;ui:{a..b}. e(i)) = u)
[iter_via_intseg_all_units]
cites the following:
1Thm*  P:(Prop). 
Thm*  (a:b:{...a}. P(a,b))
Thm*  
Thm*  (a:b:{a+1...}. (c:{a..b}. P(a,c))  P(a,b))  (a,b:P(a,b))
[all_int_segs_by_upper_ind]
0Thm*  f:(AAA), u:Aa,b:e:({a..b}A).
Thm*  ba  (Iter(f;ui:{a..b}. e(i)) = u
[iter_via_intseg_null]
1Thm*  f:(AAA), u:Aa,b:e:({a..b}A).
Thm*  a<b
Thm*  
Thm*  (Iter(f;ui:{a..b}. e(i)) = f((Iter(f;ui:{a..b-1}. e(i)),e(b-1))
[iter_via_intseg_split_last]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops Sections DiscrMathExt Doc