---

Step * 2 of Lemma bdd-diff_functionality


1. x1 : ℕ+ ⟶ ℤ@i
2. x2 : ℕ+ ⟶ ℤ@i
3. y1 : ℕ+ ⟶ ℤ@i
4. y2 : ℕ+ ⟶ ℤ@i
5. bdd-diff(x1;x2)@i
6. bdd-diff(y1;y2)@i
7. bdd-diff(x2;y2)@i
8. Refl(ℕ+ ⟶ ℤ;f,g.bdd-diff(f;g))
9. Sym(ℕ+ ⟶ ℤ;f,g.bdd-diff(f;g))
10. Trans(ℕ+ ⟶ ℤ;f,g.bdd-diff(f;g))
⊢ bdd-diff(x1;y1)
BY
{ UseTrans ⌜x2⌝⋅ }

---

Latex:

---

Latex:

1.  x1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
2.  x2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
3.  y1  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
4.  y2  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}@i
5.  bdd-diff(x1;x2)@i
6.  bdd-diff(y1;y2)@i
7.  bdd-diff(x2;y2)@i
8.  Refl(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{};f,g.bdd-diff(f;g))
9.  Sym(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{};f,g.bdd-diff(f;g))
10.  Trans(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{};f,g.bdd-diff(f;g))
\mvdash{}  bdd-diff(x1;y1)


By

---

Latex:
UseTrans  \mkleeneopen{}x2\mkleeneclose{}\mcdot{}

---

Home Index