---

Step * 1 1 1 2 1 1 of Lemma wfbts_wf


1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
⊢ (∀i:ℕ||[]||. (↑wf-term(arity;sort;snd([][i])))) ⇒ ([] ∈ (varname() List × wfterm(opr;sort;arity)) List)
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  opr  :  Type
2.  sort  :  term(opr)  {}\mrightarrow{}  \mBbbN{}
3.  arity  :  opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List)
\mvdash{}  (\mforall{}i:\mBbbN{}||[]||.  (\muparrow{}wf-term(arity;sort;snd([][i]))))
{}\mRightarrow{}  ([]  \mmember{}  (varname()  List  \mtimes{}  wfterm(opr;sort;arity))  List)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index