---

Step * of Lemma term-ind_wf

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ]. ∀[varcase:∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)]].
∀[mktermcase:∀f:opr. ∀bts:bound-term(opr) List.  ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)])]. ∀[t:term(opr)].
  (term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) ∈ P[t])
BY
{ ((Intros THEN Unhide)
   THEN (Subst' term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t) 
         ~ TERMOF{term-induction1-ext:o, \\v:l, i:l} varcase mktermcase t 0
         THENA Computation
         )
   THEN GenConcl ⌜TERMOF{term-induction1-ext:o, \\v:l, i:l}
                  = F
                  ∈ ((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
                    ⇒ (∀f:opr. ∀bts:bound-term(opr) List.  ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)]))
                    ⇒ {∀t:term(opr). P[t]})⌝⋅
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Intros  THEN  Unhide)
  THEN  (Subst'  term-ind(x.varcase[x];f,bts,r.mktermcase[f;bts;r];t)  \msim{}  TERMOF\{term-induction1-ext:o,
                                                                                                                                                        \mbackslash{}\mbackslash{}v:l,
                                                                                                                                                        i:l\} 
                                                                                                                                          varcase 
                                                                                                                                          mktermcase 
                                                                                                                                          t  0
              THENA  Computation
              )
  THEN  GenConcl  \mkleeneopen{}TERMOF\{term-induction1-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  =  F\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index