---

Step * of Lemma extend_permf_wf

∀n:ℕ. ∀p:ℕn ⟶ ℕn.  (extend_permf(p;n) ∈ ℕn + 1 ⟶ ℕn + 1)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}n:\mBbbN{}.  \mforall{}p:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}n.    (extend\_permf(p;n)  \mmember{}  \mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbN{}n  +  1)


By

---

Latex:
ProveWfLemma

---

Home Index