---

Step * of Lemma wfterm-hered-correct-sort-arity

No Annotations
∀[opr:Type]. ∀[sort:term(opr) ⟶ ℕ]. ∀[arity:opr ⟶ ((ℕ × ℕ) List)].
  wfterm(opr;sort;arity) ≡ hered-term(opr;t.correct-sort-arity(sort;arity;t))
BY
{ ((InstLemma `wf-term-hereditarily-correct-sort-arity` [] THEN RepeatFor 3 (ParallelLast'))
   THEN RepeatFor 2 (D 0)
   THEN Auto) }

---

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)  \mequiv{}  hered-term(opr;t.correct-sort-arity(sort;arity;t))


By

---

Latex:
((InstLemma  `wf-term-hereditarily-correct-sort-arity`  []  THEN  RepeatFor  3  (ParallelLast'))
  THEN  RepeatFor  2  (D  0)
  THEN  Auto)

---

Home Index