---

Step * 1 of Lemma term-induction1


1. [opr] : Type
2. [P] : term(opr) ⟶ ℙ
3. ∀v:{v:varname()| ¬(v = nullvar() ∈ varname())} . P[varterm(v)]
4. ∀f:opr. ∀bts:bound-term(opr) List.  ((∀i:ℕ||bts||. P[snd(bts[i])]) ⇒ P[mkterm(f;bts)])
5. [n] : ℕ
6. term(opr) ≡ coterm-fun(opr;term(opr))
7. y1 : opr
8. y2 : (varname() List × term(opr)) List
9. inr <y1, y2>  ∈ term(opr)
10. (1 + Σ(term-size(snd(bt)) | bt ∈ y2)) ≤ n
11. 1 ≤ (1 + Σ(term-size(snd(bt)) | bt ∈ y2))
12. ∀a:{a:term(opr)| term-size(a) ≤ (n - 1)} . P[a]
13. i : ℕ||y2||
⊢ P[snd(y2[i])]
BY
{ (BackThruSomeHyp
   THEN InstLemma `summand-le-lsum` [⌜varname() List × term(opr)⌝;⌜y2⌝;⌜λ2bt.term-size(snd(bt))⌝;⌜y2[i]⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [opr]  :  Type
2.  [P]  :  term(opr)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}v:\{v:varname()|  \mneg{}(v  =  nullvar())\}  .  P[varterm(v)]
4.  \mforall{}f:opr.  \mforall{}bts:bound-term(opr)  List.    ((\mforall{}i:\mBbbN{}||bts||.  P[snd(bts[i])])  {}\mRightarrow{}  P[mkterm(f;bts)])
5.  [n]  :  \mBbbN{}
6.  term(opr)  \mequiv{}  coterm-fun(opr;term(opr))
7.  y1  :  opr
8.  y2  :  (varname()  List  \mtimes{}  term(opr))  List
9.  inr  <y1,  y2>    \mmember{}  term(opr)
10.  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2))  \mleq{}  n
11.  1  \mleq{}  (1  +  \mSigma{}(term-size(snd(bt))  |  bt  \mmember{}  y2))
12.  \mforall{}a:\{a:term(opr)|  term-size(a)  \mleq{}  (n  -  1)\}  .  P[a]
13.  i  :  \mBbbN{}||y2||
\mvdash{}  P[snd(y2[i])]


By

---

Latex:
(BackThruSomeHyp
  THEN  InstLemma  `summand-le-lsum`  [\mkleeneopen{}varname()  List  \mtimes{}  term(opr)\mkleeneclose{};\mkleeneopen{}y2\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}bt.term-size(snd(bt))\mkleeneclose{};
  \mkleeneopen{}y2[i]\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index