Nuprl - IteratedBinops LEMMAs for iter_via_intseg_all

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Rank	Theorem	Name
2	Thm* f:(AAA), u:A. Thm* is_ident(A; f; u) Thm* Thm* (a,b:, e:({a..b}A). Thm* ((i:{a..b}. e(i) = u) (Iter(f;u) i:{a..b}. e(i)) = u)	[iter_via_intseg_all_units]
cites the following:
1	Thm* 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]
0	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* ba (Iter(f;u) i:{a..b}. e(i)) = u	[iter_via_intseg_null]
1	Thm* f:(AAA), u:A, a,b:, e:({a..b}A). Thm* a<b Thm* Thm* (Iter(f;u) i:{a..b}. e(i)) = f((Iter(f;u) i:{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