---

Step * of Lemma ctt-term-induction

No Annotations
∀[P:CttTerm ⟶ ℙ{i'''''}]
  ((∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)])
  ⇒ (∀f:CttOp. ∀bts:{bts:(varname() List × CttTerm) List| 
                      (||bts|| = ||ctt-arity(f)|| ∈ ℤ)
                      ∧ (∀i:ℕ||bts||
                           ((||fst(bts[i])|| = (fst(ctt-arity(f)[i])) ∈ ℤ)
                           ∧ (ctt-kind(snd(bts[i])) = (snd(ctt-arity(f)[i])) ∈ ℤ)))} .
        ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkwfterm(f;bts)]))
  ⇒ {∀t:CttTerm. P[t]})
BY
{ ((InstLemma `wf-term-induction` [⌜parm{i'''''}⌝;⌜CttOp⌝;⌜λt.ctt-kind(t)⌝;⌜λx.ctt-arity(x)⌝]⋅ THENA Auto)
   THEN Unfold `wf-bound-terms` -1
   THEN Fold `ctt-term` (-1)
   THEN Reduce -1
   THEN Trivial) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[P:CttTerm  {}\mrightarrow{}  \mBbbP{}\{i'''''\}]
    ((\mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .  P[varterm(v)])
    {}\mRightarrow{}  (\mforall{}f:CttOp.  \mforall{}bts:\{bts:(varname()  List  \mtimes{}  CttTerm)  List| 
                                            (||bts||  =  ||ctt-arity(f)||)
                                            \mwedge{}  (\mforall{}i:\mBbbN{}||bts||
                                                      ((||fst(bts[i])||  =  (fst(ctt-arity(f)[i])))
                                                      \mwedge{}  (ctt-kind(snd(bts[i]))  =  (snd(ctt-arity(f)[i])))))\}  .
                ((\mforall{}i:\mBbbN{}||bts||.  P[snd(bts[i])])  {}\mRightarrow{}  P[mkwfterm(f;bts)]))
    {}\mRightarrow{}  \{\mforall{}t:CttTerm.  P[t]\})


By

---

Latex:
((InstLemma  `wf-term-induction`  [\mkleeneopen{}parm\{i'''''\}\mkleeneclose{};\mkleeneopen{}CttOp\mkleeneclose{};\mkleeneopen{}\mlambda{}t.ctt-kind(t)\mkleeneclose{};\mkleeneopen{}\mlambda{}x.ctt-arity(x)\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  Unfold  `wf-bound-terms`  -1
  THEN  Fold  `ctt-term`  (-1)
  THEN  Reduce  -1
  THEN  Trivial)

---

Home Index