---

Step * of Lemma bdd-diff_functionality

∀x1,x2,y1,y2:ℕ+ ⟶ ℤ.  (bdd-diff(x1;x2) ⇒ bdd-diff(y1;y2) ⇒ (bdd-diff(x1;y1) ⇐⇒ bdd-diff(x2;y2)))
BY
{ (Auto THEN InstLemma `bdd-diff-equiv` [] THEN D -1 THEN Auto) }

1
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(x1;y1)@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(x2;y2)

2
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)

---

Latex:

---

Latex:
\mforall{}x1,x2,y1,y2:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.    (bdd-diff(x1;x2)  {}\mRightarrow{}  bdd-diff(y1;y2)  {}\mRightarrow{}  (bdd-diff(x1;y1)  \mLeftarrow{}{}\mRightarrow{}  bdd-diff(x2;y2)))


By

---

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

---

Home Index