---

Step * 1 2 of Lemma nat_add_mon_wf2

.....wf..... 
λx.x ∈ |<ℕ,+>| ⟶ |<ℤ+>|
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
\mlambda{}x.x  \mmember{}  |<\mBbbN{},+>|  {}\mrightarrow{}  |<\mBbbZ{}+>|


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index