---

Step * of Lemma wf-bound-terms_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index