---

Step * 1 5 of Lemma nat_add_mon_wf2


RelsIso(|<ℕ,+>|;|<ℤ+>|;x,y.↑(x ≤b y);x,y.↑(x ≤b y);λx.x)
BY
{ AGenRepD ["basic";"compound"] THEN All Reduce THEN Auto⋅ }

---

Latex:

---

Latex:

RelsIso(|<\mBbbN{},+>|;|<\mBbbZ{}+>|;x,y.\muparrow{}(x  \mleq{}\msubb{}  y);x,y.\muparrow{}(x  \mleq{}\msubb{}  y);\mlambda{}x.x)


By

---

Latex:
AGenRepD  ["basic";"compound"]  THEN  All  Reduce  THEN  Auto\mcdot{}

---

Home Index