---

Step * of Lemma weakly-safe-seq_wf

∀[R:ℕ ⟶ ℕ ⟶ ℙ]. ∀[n:ℕ]. ∀[s:ℕn ⟶ ℕ].  (weakly-safe-seq(R;n;s) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[R:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  \mBbbN{}].    (weakly-safe-seq(R;n;s)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index