IteratedBinops Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  is_commutative_sep(A; f) == is_commutative(A; x,z.(f(x,z)))

is mentioned by

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)		[iter_via_intseg_comp_binop]
Thm*  is_commutative_sep(; (x,y. x+y))[is_commutative_sep_intadd]
Thm*  is_commutative_sep(; (x,y. xy))[is_commutative_sep_intmul]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

IteratedBinops Sections DiscrMathExt Doc