---

Step * of Lemma wf-term-hereditarily-correct-sort-arity

No Annotations
∀[opr:Type]
  ∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List). ∀t:term(opr).
    (↑wf-term(arity;sort;t) ⇐⇒ hereditarily(opr;s.correct-sort-arity(sort;arity;s);t))
BY
{ RepeatFor 3 (Intro) }

1
1. [opr] : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
⊢ ∀t:term(opr). (↑wf-term(arity;sort;t) ⇐⇒ hereditarily(opr;s.correct-sort-arity(sort;arity;s);t))

---

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).
        (\muparrow{}wf-term(arity;sort;t)  \mLeftarrow{}{}\mRightarrow{}  hereditarily(opr;s.correct-sort-arity(sort;arity;s);t))


By

---

Latex:
RepeatFor  3  (Intro)

---

Home Index