---

Step * of Lemma baf-bar_wf

∀[R,T:ℕ ⟶ ℕ ⟶ ℙ]. ∀[l:ℕ]. ∀[a:x:ℕl ⟶ ℕ].  (baf-bar(n,m.R[n;m];n,m.T[n;m];l;a) ∈ ℙ)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[R,T:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[l:\mBbbN{}].  \mforall{}[a:x:\mBbbN{}l  {}\mrightarrow{}  \mBbbN{}].    (baf-bar(n,m.R[n;m];n,m.T[n;m];l;a)  \mmember{}  \mBbbP{})


By

---

Latex:
ProveWfLemma

---

Home Index