---

Step * of Lemma add-swap

∀[x:ℤ]. ∀[y,z:Top].  (x + y + z ~ y + x + z)
BY
{ ((UnivCD THENA Auto)
   THEN (RW (AddrC [1] (RevLemmaC `add-associates`)) 0 THENA Trivial)
   THEN (RW (AddrC [1;1] (LemmaC `add-commutes`)) 0 THENA Trivial)
   THEN (RW (AddrC [1] (LemmaC `add-associates`)) 0 THENA Trivial)) }

1
1. x : ℤ
2. y : Top
3. z : Top
⊢ y + x + z ~ y + x + z

---

Latex:

---

Latex:
\mforall{}[x:\mBbbZ{}].  \mforall{}[y,z:Top].    (x  +  y  +  z  \msim{}  y  +  x  +  z)


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RW  (AddrC  [1]  (RevLemmaC  `add-associates`))  0  THENA  Trivial)
  THEN  (RW  (AddrC  [1;1]  (LemmaC  `add-commutes`))  0  THENA  Trivial)
  THEN  (RW  (AddrC  [1]  (LemmaC  `add-associates`))  0  THENA  Trivial))

---

Home Index