---

Step * of Lemma primrec-wf-int_seg

∀[a,b:ℤ].
  ∀[P:{a..b-} ⟶ ℙ]. ∀[init:P[a]]. ∀[s:∀n:ℕb - 1 - a. (P[a + n] ⇒ P[a + n + 1])]. ∀[n:{a..b-}].
    (primrec(n - a;init;s) ∈ P[n]) 
  supposing a < b
BY
{ (Auto
   THEN (Assert ⌜∀d:ℕ. (d < b - a ⇒ (primrec(d;init;s) ∈ P[a + d]))⌝⋅ THENM (InstHyp [⌜n - a⌝] (-1)⋅ THEN Auto))
   THEN InductionOnNat
   THEN (RWO "primrec-unroll" 0 THENA Auto)
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbZ{}].
    \mforall{}[P:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[init:P[a]].  \mforall{}[s:\mforall{}n:\mBbbN{}b  -  1  -  a.  (P[a  +  n]  {}\mRightarrow{}  P[a  +  n  +  1])].  \mforall{}[n:\{a..b\msupminus{}\}].
        (primrec(n  -  a;init;s)  \mmember{}  P[n]) 
    supposing  a  <  b


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  (d  <  b  -  a  {}\mRightarrow{}  (primrec(d;init;s)  \mmember{}  P[a  +  d]))\mkleeneclose{}\mcdot{}
  THENM  (InstHyp  [\mkleeneopen{}n  -  a\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index