---

Step * of Lemma add-has-value-iff

∀[x,y:partial(ℕ)].  uiff((x + y)↓;(x)↓ ∧ (y)↓)
BY
{ (Intros THEN (RepeatFor 2 (D 0) THENA Auto)) }

1
1. x : partial(ℕ)
2. y : partial(ℕ)
3. (x + y)↓
⊢ (x)↓ ∧ (y)↓

2
1. x : partial(ℕ)
2. y : partial(ℕ)
3. (x)↓ ∧ (y)↓
⊢ (x + y)↓

---

Latex:

---

Latex:
\mforall{}[x,y:partial(\mBbbN{})].    uiff((x  +  y)\mdownarrow{};(x)\mdownarrow{}  \mwedge{}  (y)\mdownarrow{})


By

---

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

---

Home Index