---

Step * of Lemma mset_for_swap

∀g:IAbMonoid. ∀s,s':DSet. ∀f:|s| ⟶ |s'| ⟶ |g|. ∀a:MSet{s}. ∀b:MSet{s'}.
  ((msFor{g} x ∈ a. msFor{g} y ∈ b. f[x;y]) = (msFor{g} y ∈ b. msFor{g} x ∈ a. f[x;y]) ∈ |g|)
BY
{ ((CDToVarThen `f' (\i.RW mset_elimC 0) 
THENM Backchain ``mon_for_swap``) THENA Auto) }

---

Latex:

---

Latex:
\mforall{}g:IAbMonoid.  \mforall{}s,s':DSet.  \mforall{}f:|s|  {}\mrightarrow{}  |s'|  {}\mrightarrow{}  |g|.  \mforall{}a:MSet\{s\}.  \mforall{}b:MSet\{s'\}.
    ((msFor\{g\}  x  \mmember{}  a.  msFor\{g\}  y  \mmember{}  b.  f[x;y])  =  (msFor\{g\}  y  \mmember{}  b.  msFor\{g\}  x  \mmember{}  a.  f[x;y]))


By

---

Latex:
((CDToVarThen  `f'  (\mbackslash{}i.RW  mset\_elimC  0) 
THENM  Backchain  ``mon\_for\_swap``)  THENA  Auto)

---

Home Index