---

Step * of Lemma wfterm_wf

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)].  (wfterm(opr;sort;arity) ∈ Type)
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[sort:term(opr)  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)].
    (wfterm(opr;sort;arity)  \mmember{}  Type)


By

---

Latex:
ProveWfLemma

---

Home Index