---

Step * of Lemma term-induction1

No Annotations
∀[opr:Type]. ∀[P:term(opr) ⟶ ℙ].
  ((∀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]})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN (Enough to prove ∀[n:ℕ]. ∀a:{a:term(opr)| term-size(a) ≤ n} . P[a]
          Because (InstHyp [⌜term-size(t)⌝;⌜t⌝] (-1)⋅ THEN Auto))
   THEN Thin (-1)
   THEN (UniformCompNatInd THENW Auto)
   THEN Intro
   THEN (InstLemma `term-ext` [⌜opr⌝]⋅ THENA Auto)
   THEN (Assert term-size(a) ≤ n BY
               Auto)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜a = t ∈ coterm-fun(opr;term(opr))⌝⋅ THENA Auto)
   THEN ThinVar `a'
   THEN (Assert t ∈ term(opr) BY
               Auto)
   THEN RepeatFor 2 (D -2)
   THEN Folds  ``varterm mkterm`` 0
   THEN Reduce 0
   THEN Auto
   THEN ((Assert 1 ≤ term-size(mkterm(y1;y2)) BY Auto) THEN Reduce -1)
   THEN (D 6 With ⌜n - 1⌝  THENA Auto)
   THEN BHyp 4
   THEN Auto) }

1
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])]

---

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{}f:opr.  \mforall{}bts:bound-term(opr)  List.    ((\mforall{}i:\mBbbN{}||bts||.  P[snd(bts[i])])  {}\mRightarrow{}  P[mkterm(f;bts)]))
    {}\mRightarrow{}  \{\mforall{}t:term(opr).  P[t]\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  (Enough  to  prove  \mforall{}[n:\mBbbN{}].  \mforall{}a:\{a:term(opr)|  term-size(a)  \mleq{}  n\}  .  P[a]
                Because  (InstHyp  [\mkleeneopen{}term-size(t)\mkleeneclose{};\mkleeneopen{}t\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto))
  THEN  Thin  (-1)
  THEN  (UniformCompNatInd  THENW  Auto)
  THEN  Intro
  THEN  (InstLemma  `term-ext`  [\mkleeneopen{}opr\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  term-size(a)  \mleq{}  n  BY
                          Auto)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}a  =  t\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `a'
  THEN  (Assert  t  \mmember{}  term(opr)  BY
                          Auto)
  THEN  RepeatFor  2  (D  -2)
  THEN  Folds    ``varterm  mkterm``  0
  THEN  Reduce  0
  THEN  Auto
  THEN  ((Assert  1  \mleq{}  term-size(mkterm(y1;y2))  BY  Auto)  THEN  Reduce  -1)
  THEN  (D  6  With  \mkleeneopen{}n  -  1\mkleeneclose{}    THENA  Auto)
  THEN  BHyp  4
  THEN  Auto)

---

Home Index