Nuprl - IteratedBinops LEMMAs for iter_via_intseg

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

Rank	Theorem	Name
3	Thm* f:(AAA), u:A, a,b,c,d:. Thm* b-a = d-c Thm* Thm* (e:({a..b}A), g:({c..d}A). Thm* ((i:{a..b}, j:{c..d}. j-i = c-a e(i) = g(j) A) Thm* ( Thm* ((Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{c..d}. g(j)))	[iter_via_intseg_shift]
cites the following:
2	Thm* f:(AAA), u:A, a,b:, e:({a..b}A), k:. Thm* (Iter(f;u) i:{a..b}. e(i)) = (Iter(f;u) j:{a+k..b+k}. e(j-k))	[iter_via_intseg_shift_rw]

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