---

Step * of Lemma bdd-diff_inversion

∀a,b:ℕ+ ⟶ ℤ.  (bdd-diff(a;b) ⇒ bdd-diff(b;a))
BY
{ (InstLemma `bdd-diff-equiv` [] THEN Auto)⋅ }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(a;b)  {}\mRightarrow{}  bdd-diff(b;a))


By

---

Latex:
(InstLemma  `bdd-diff-equiv`  []  THEN  Auto)\mcdot{}

---

Home Index