---

Step * of Lemma bdd-diff-equiv

EquivRel(ℕ+ ⟶ ℤ;f,g.bdd-diff(f;g))
BY
{ RepeatFor 2 ((D 0 THEN Auto)) }

1
1. a : ℕ+ ⟶ ℤ
⊢ bdd-diff(a;a)

2
1. a : ℕ+ ⟶ ℤ
2. b : ℕ+ ⟶ ℤ
3. bdd-diff(a;b)
⊢ bdd-diff(b;a)

3
1. Sym(ℕ+ ⟶ ℤ;f,g.bdd-diff(f;g))
2. a : ℕ+ ⟶ ℤ
3. b : ℕ+ ⟶ ℤ
4. c : ℕ+ ⟶ ℤ
5. bdd-diff(a;b)
6. bdd-diff(b;c)
⊢ bdd-diff(a;c)

---

Latex:

---

Latex:
EquivRel(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{};f,g.bdd-diff(f;g))


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Auto))

---

Home Index