When the default empty-range value is an identity value for the binary operation, i.e.

Def  is_ident(A; f; u) == x:A. f(u,x) = x & f(x,u) = x

which incidentally is unique if it exists; and when, further, the binary operation is associative then the range of iteration {a..b} can be freely split into two subranges, {a..c} and {c..b}, as described in the following theorem:

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)))

If the binary operation, in addition to having an identity and being associative, is commutative,

Def  is_commutative_sep(A; f) == is_commutative(A; x,z.(f(x,z)))

then iterations over two sets of values, e and g in {a..b}A, indexed by the same integer subrange, can be easily combined pointwise by the binary operation f  AAA:

Thm*  f:(AAA), u:A.
Thm*  is_commutative_sep(A; f)
Thm*  
Thm*  is_ident(A; f; u)
Thm*  
Thm*  is_assoc_sep(A; f)
Thm*  
Thm*  (a,b:, e,g:({a..b}A).
Thm*  (f((Iter(f;u) i:{a..b}. e(i)),Iter(f;u) i:{a..b}. g(i))
Thm*  (=
Thm*  ((Iter(f;u) i:{a..b}. f(e(i),g(i)))
Thm*  ( A)

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