Nuprl - IteratedBinops LEMMAs for sum

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

Rank	Theorem	Name
4	Thm* i:, x,y:. ixiy = i(x+y)	[sum_exponent]
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]
3	Thm* a,c,b:, e:({a..b}). Thm* ac Thm* Thm* cb ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))	[mul_via_intseg_split_mid]

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