---

Step * of Lemma term-induction

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
  ((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
  ⇒ (∀bts:bound-term(opr) List. ((∀bt:bound-term(opr). ((bt ∈ bts) ⇒ P[snd(bt)])) ⇒ (∀f:opr. P[mkterm(f;bts)])))
  ⇒ {∀t:term(opr). P[t]})
BY
{ (Unfold `guard` 0
   THEN Intros
   THEN RenameVar `v' 3
   THEN RenameVar `m' 4
   THEN (InstLemma `term-ind_wf` [⌜opr⌝;⌜P⌝]⋅ THENA Auto)
   THEN UseWitness ⌜term-ind(x.v x;f,bts,r.m bts (λbt,x. let i,_,_ = x in r i) f;t)⌝⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Unfold  `guard`  0
  THEN  Intros
  THEN  RenameVar  `v'  3
  THEN  RenameVar  `m'  4
  THEN  (InstLemma  `term-ind\_wf`  [\mkleeneopen{}opr\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  UseWitness  \mkleeneopen{}term-ind(x.v  x;f,bts,r.m  bts  (\mlambda{}bt,x.  let  i,$_{}$,$_\mbackslash{}ff\000C7b}$  =  x  in  r  i)  f;t)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index