---

Step * of Lemma retraction-nat-nsub

∀k:ℕ+. ∃r:ℕ ⟶ ℕk. ∀x:ℕk. ((r x) = x ∈ ℕk)
BY
{ (Auto THEN D 0 With ⌜λx.if x <z k then x else 0 fi ⌝  THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}\msupplus{}.  \mexists{}r:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}k.  \mforall{}x:\mBbbN{}k.  ((r  x)  =  x)


By

---

Latex:
(Auto  THEN  D  0  With  \mkleeneopen{}\mlambda{}x.if  x  <z  k  then  x  else  0  fi  \mkleeneclose{}    THEN  Reduce  0  THEN  Auto)

---

Home Index