---

Step * 1 1 of Lemma radd-list_functionality


1. 0 = 0 ∈ ℤ
2. ∀i:ℕ0. (⊥ = ⊥)
⊢ bdd-diff(λn.0;λn.0)
BY
{ (RelRST THEN Auto) }

---

Latex:

---

Latex:

1.  0  =  0
2.  \mforall{}i:\mBbbN{}0.  (\mbot{}  =  \mbot{})
\mvdash{}  bdd-diff(\mlambda{}n.0;\mlambda{}n.0)


By

---

Latex:
(RelRST  THEN  Auto)

---

Home Index