---

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


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)
BY
{ (D -1 With ⌜0⌝  THENA 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. ↑wf-term(arity;sort;snd([<u1, u2> / v][0]))
⊢ u2 ∈ wfterm(opr;sort;arity)

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1  With  \mkleeneopen{}0\mkleeneclose{}    THENA  Auto)

---

Home Index