---

Step * 1 1 1 2 1 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)
⊢ (∀i:ℕ||[u / v]||. (↑wf-term(arity;sort;snd([u / v][i]))))
⇒ ([u / v] ∈ (varname() List × wfterm(opr;sort;arity)) List)
BY
{ Auto }

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

2
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

---

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)
\mvdash{}  (\mforall{}i:\mBbbN{}||[u  /  v]||.  (\muparrow{}wf-term(arity;sort;snd([u  /  v][i]))))
{}\mRightarrow{}  ([u  /  v]  \mmember{}  (varname()  List  \mtimes{}  wfterm(opr;sort;arity))  List)


By

---

Latex:
Auto

---

Home Index