---

Step * of Lemma correct-sort-arity_wf

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

---

Latex:

---

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


By

---

Latex:
ProveWfLemma

---

Home Index