---

Step * of Lemma integer-induction

∀[P:ℤ ⟶ ℙ]. (P[0] ⇒ (∀y:{x:ℤ| 0 < x} . (P[y - 1] ⇒ P[y])) ⇒ (∀y:{x:ℤ| x < 0} . (P[y + 1] ⇒ P[y])) ⇒ (∀x:ℤ. P[x]))
BY
{ (Auto
   THEN RenameVar `b' 2
   THEN RenameVar `s' 3
   THEN RenameVar `p' 4
   THEN UseWitness ⌜if x <z 0 then primrec(-x;b;λi,x. ((λn.(p (-n))) (i + 1) x)) else primrec(x;b;λi,x. (s (i + 1) x)) f\000Ci ⌝⋅
   THEN (BoolCase ⌜x <z 0⌝⋅ THENA Auto)) }

1
1. P : ℤ ⟶ ℙ
2. b : P[0]
3. s : ∀y:{x:ℤ| 0 < x} . (P[y - 1] ⇒ P[y])
4. p : ∀y:{x:ℤ| x < 0} . (P[y + 1] ⇒ P[y])
5. x : ℤ
6. x < 0
⊢ primrec(-x;b;λi,x. (p (-(i + 1)) x)) ∈ P[x]

2
1. P : ℤ ⟶ ℙ
2. b : P[0]
3. s : ∀y:{x:ℤ| 0 < x} . (P[y - 1] ⇒ P[y])
4. p : ∀y:{x:ℤ| x < 0} . (P[y + 1] ⇒ P[y])
5. x : ℤ
6. ¬x < 0
⊢ primrec(x;b;λi,x. (s (i + 1) x)) ∈ P[x]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbZ{}  {}\mrightarrow{}  \mBbbP{}]
    (P[0]
    {}\mRightarrow{}  (\mforall{}y:\{x:\mBbbZ{}|  0  <  x\}  .  (P[y  -  1]  {}\mRightarrow{}  P[y]))
    {}\mRightarrow{}  (\mforall{}y:\{x:\mBbbZ{}|  x  <  0\}  .  (P[y  +  1]  {}\mRightarrow{}  P[y]))
    {}\mRightarrow{}  (\mforall{}x:\mBbbZ{}.  P[x]))


By

---

Latex:
(Auto
  THEN  RenameVar  `b'  2
  THEN  RenameVar  `s'  3
  THEN  RenameVar  `p'  4
  THEN  UseWitness  \mkleeneopen{}if  x  <z  0
                                    then  primrec(-x;b;\mlambda{}i,x.  ((\mlambda{}n.(p  (-n)))  (i  +  1)  x))
                                    else  primrec(x;b;\mlambda{}i,x.  (s  (i  +  1)  x))
                                    fi  \mkleeneclose{}\mcdot{}
  THEN  (BoolCase  \mkleeneopen{}x  <z  0\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index