Nuprl - IteratedBinops LEMMAs for iter_via_intseg_split

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

Rank	Theorem	Name
3	Thm* f:(AAA), u:A. Thm* is_ident(A; f; u) Thm* Thm* is_assoc_sep(A; f) Thm* Thm* (a,c,b:, e:({a..b}A). Thm* (ac Thm* ( Thm* (c<b Thm* ( Thm* ((Iter(f;u) i:{a..b}. e(i)) Thm* (= Thm* (f((Iter(f;u) i:{a..c}. e(i)),f(e(c),Iter(f;u) i:{c+1..b}. e(i))))	[iter_via_intseg_split_pluck]
cites the following:
2	Thm* f:(AAA), u:A. Thm* is_ident(A; f; u) Thm* Thm* is_assoc_sep(A; f) Thm* Thm* (a,c,b:, e:({a..b}A). Thm* (ac Thm* ( Thm* (cb Thm* ( Thm* ((Iter(f;u) i:{a..b}. e(i)) Thm* (= Thm* (f((Iter(f;u) i:{a..c}. e(i)),Iter(f;u) i:{c..b}. e(i)))	[iter_via_intseg_split_mid]
0	Thm* f:(AAA), u:A. Thm* is_ident(A; f; u) Thm* Thm* (a,b:, e:({a..b}A). a+1 = b (Iter(f;u) i:{a..b}. e(i)) = e(a))	[iter_via_intseg_singleton]

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