---

Step * of Lemma bound-term-induction

No Annotations
∀[opr:Type]. ∀[P:bound-term(opr) ⟶ ℙ].
  ((∀vs:varname() List. ∀v:varname().  ((¬(v = nullvar() ∈ varname())) ⇒ P[<vs, varterm(v)>]))
  ⇒ (∀bts:bound-term(opr) List
        ((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[bt])) ⇒ (∀f:opr. ∀vs:varname() List.  P[<vs, mkterm(f;bts)>])))
  ⇒ (∀bt:bound-term(opr). P[bt]))
BY
{ Auto }

1
1. [opr] : Type
2. [P] : bound-term(opr) ⟶ ℙ
3. ∀vs:varname() List. ∀v:varname().  ((¬(v = nullvar() ∈ varname())) ⇒ P[<vs, varterm(v)>])
4. ∀bts:bound-term(opr) List
     ((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[bt])) ⇒ (∀f:opr. ∀vs:varname() List.  P[<vs, mkterm(f;bts)>]))
5. bt : bound-term(opr)
⊢ P[bt]

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type].  \mforall{}[P:bound-term(opr)  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}vs:varname()  List.  \mforall{}v:varname().    ((\mneg{}(v  =  nullvar()))  {}\mRightarrow{}  P[<vs,  varterm(v)>]))
    {}\mRightarrow{}  (\mforall{}bts:bound-term(opr)  List
                ((\mforall{}bt:bound-term(opr).  ((bt  \mmember{}  bts)  {}\mRightarrow{}  P[bt]))
                {}\mRightarrow{}  (\mforall{}f:opr.  \mforall{}vs:varname()  List.    P[<vs,  mkterm(f;bts)>])))
    {}\mRightarrow{}  (\mforall{}bt:bound-term(opr).  P[bt]))


By

---

Latex:
Auto

---

Home Index