(def-theorem associative-law-for-multiplication-for-monoids
*Remark: This entry is multiply defined. See: [1] [2]*
associative-law-for-multiplication-for-monoids
(usages transportable-macete)
(theory monoid-theory)
(proof existing-theorem))

(def-theorem reverse-associative-law-for-multiplication-for-monoids
*"forall(z,y,x:uu, (x**y)**z = x**(y**z))"*
(theory monoid-theory)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids)
simplify
)))

(def-theorem left-cancellation-law-for-monoids
*"forall(x,y,z:uu, y = z implies x**y = x**z)"*
(theory monoid-theory)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
)
))

(def-theorem right-cancellation-law-for-monoids
*"forall(x,y,z:uu, x = y implies x**z = y**z)"*
(usages transportable-macete)
(theory monoid-theory)
(proof
(
direct-and-antecedent-inference-strategy
)
))

(def-compound-macete monoid-cancellation-laws
(series
(repeat
reverse-associative-law-for-multiplication-for-monoids
tr%reverse-associative-law-for-multiplication-for-monoids)
(repeat
left-cancellation-law-for-monoids
tr%left-cancellation-law-for-monoids)
(repeat
associative-law-for-multiplication-for-monoids
tr%associative-law-for-multiplication-for-monoids)
(repeat
right-cancellation-law-for-monoids
tr%right-cancellation-law-for-monoids)))

(def-theorem monoid%prod-distributes-over-**
*"forall(m,n:zz,f,g:[zz,uu],
m<=n and forall(k:zz, m<=k and k<=n implies #(f(k)) and #(g(k)))
implies
monoid%prod(m,n,lambda(i:zz,f(i)**g(i))) =
monoid%prod(m,n,f) ** monoid%prod(m,n,g))"*
(theory commutative-monoid-theory)
(usages transportable-macete)
(proof
(
(induction integer-inductor (*"n"*))
(backchain *"with(p:prop,p implies p)"*)
direct-and-antecedent-inference-strategy
simplify
simplify
(apply-macete-with-minor-premises monoid-cancellation-laws)
(apply-macete-locally commutative-law-for-monoids
(0)
*"monoid%prod(m,t,g)**f(1+t)"*)
simplify
simplify
simplify
)))