---

Step * of Lemma bdd-diff_transitivity

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

---

Latex:

---

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


By

---

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

---

Home Index