---

Step * 1 1 1 2 1 2 2 of Lemma wfbts_wf


1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. u : bound-term(opr)
5. v : bound-term(opr) List
6. (∀i:ℕ||v||. (↑wf-term(arity;sort;snd(v[i])))) ⇒ (v ∈ (varname() List × wfterm(opr;sort;arity)) List)
7. ∀i:ℕ||[u / v]||. (↑wf-term(arity;sort;snd([u / v][i])))
⊢ v ∈ (varname() List × wfterm(opr;sort;arity)) List
BY
{ (BackThruSomeHyp THEN Auto) }

1
1. opr : Type
2. sort : term(opr) ⟶ ℕ
3. arity : opr ⟶ ((ℕ × ℕ) List)
4. u : bound-term(opr)
5. v : bound-term(opr) List
6. (∀i:ℕ||v||. (↑wf-term(arity;sort;snd(v[i])))) ⇒ (v ∈ (varname() List × wfterm(opr;sort;arity)) List)
7. ∀i:ℕ||[u / v]||. (↑wf-term(arity;sort;snd([u / v][i])))
8. i : ℕ||v||
⊢ ↑wf-term(arity;sort;snd(v[i]))

---

Latex:

---

Latex:

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


By

---

Latex:
(BackThruSomeHyp  THEN  Auto)

---

Home Index