IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
2Thm*  a,b:P:({a..b}Prop). (i:{a..b}. P(i))  (Or i:{a..b}. P(i))[exist_intseg_vs_iter_or]
cites the following:
0Thm*  f:(AAA), u:Aa,b:e:({a..b}A).
Thm*  ba  (Iter(f;ui:{a..b}. e(i)) = u
[iter_via_intseg_null]
0Thm*  a,b:P:({a..b}Prop). ba  (i:{a..b}. P(i))[exist_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]
1Thm*  a,b:P:({a..b}Prop).
Thm*  a<b  ((i:{a..b}. P(i))  (i:{a..(b-1)}. P(i))  P(b-1))
[or_via_exist_intseg_split_last]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops Sections DiscrMathExt Doc