---

Step * of Lemma wf-term-induction

No Annotations
∀[opr:Type]
  ∀sort:term(opr) ⟶ ℕ. ∀arity:opr ⟶ ((ℕ × ℕ) List).
    ∀[P:wfterm(opr;sort;arity) ⟶ ℙ]
      ((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
      ⇒ (∀f:opr. ∀bts:wf-bound-terms(opr;sort;arity;f).  ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)]))
      ⇒ {∀t:wfterm(opr;sort;arity). P[t]})
BY
{ (InstLemma `term-ind_wf_wfterm` []
   THEN RepeatFor 4 (ParallelLast')
   THEN Unfolds ``implies guard`` 0
   THEN Fold`all` 0
   THEN RepeatFor 3 (ParallelLast')
   THEN UseWitness ⌜term-ind(x.%[x];f,bts,r.%5[f;bts;r];t)⌝⋅
   THEN Trivial) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[opr:Type]
    \mforall{}sort:term(opr)  {}\mrightarrow{}  \mBbbN{}.  \mforall{}arity:opr  {}\mrightarrow{}  ((\mBbbN{}  \mtimes{}  \mBbbN{})  List).
        \mforall{}[P:wfterm(opr;sort;arity)  {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .  P[varterm(v)])
            {}\mRightarrow{}  (\mforall{}f:opr.  \mforall{}bts:wf-bound-terms(opr;sort;arity;f).
                        ((\mforall{}i:\mBbbN{}||bts||.  P[snd(bts[i])])  {}\mRightarrow{}  P[mkwfterm(f;bts)]))
            {}\mRightarrow{}  \{\mforall{}t:wfterm(opr;sort;arity).  P[t]\})


By

---

Latex:
(InstLemma  `term-ind\_wf\_wfterm`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  Unfolds  ``implies  guard``  0
  THEN  Fold`all`  0
  THEN  RepeatFor  3  (ParallelLast')
  THEN  UseWitness  \mkleeneopen{}term-ind(x.\%[x];f,bts,r.\%5[f;bts;r];t)\mkleeneclose{}\mcdot{}
  THEN  Trivial)

---

Home Index