---

Step * of Lemma ibs-property

∀[s:IBS]. ∀[m:ℕ].  ∀[n:ℕ]. (s n) = 1 ∈ ℤ supposing m ≤ n supposing (s m) = 1 ∈ ℤ
BY
{ (Auto
   THEN (Assert ∀d:ℕ. ((s (m + d)) = 1 ∈ ℤ) BY
               (DVar `s'
                THEN (Unhide THENA Auto)
                THEN InductionOnNat
                THEN Auto
                THEN (Subst' m + d ~ 1 + m + (d - 1) 0 THENA Auto)
                THEN (InstHyp [⌜m + (d - 1)⌝] 2⋅ THENA Auto)
                THEN (RWO "-2" (-1) THENA Auto)
                THEN MoveToConcl (-1)
                THEN GenConclTerm ⌜s (1 + m + (d - 1))⌝⋅
                THEN Auto))
   ) }

1
1. s : IBS
2. m : ℕ
3. (s m) = 1 ∈ ℤ
4. n : ℕ
5. m ≤ n
6. ∀d:ℕ. ((s (m + d)) = 1 ∈ ℤ)
⊢ (s n) = 1 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[s:IBS].  \mforall{}[m:\mBbbN{}].    \mforall{}[n:\mBbbN{}].  (s  n)  =  1  supposing  m  \mleq{}  n  supposing  (s  m)  =  1


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}d:\mBbbN{}.  ((s  (m  +  d))  =  1)  BY
                          (DVar  `s'
                            THEN  (Unhide  THENA  Auto)
                            THEN  InductionOnNat
                            THEN  Auto
                            THEN  (Subst'  m  +  d  \msim{}  1  +  m  +  (d  -  1)  0  THENA  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}m  +  (d  -  1)\mkleeneclose{}]  2\mcdot{}  THENA  Auto)
                            THEN  (RWO  "-2"  (-1)  THENA  Auto)
                            THEN  MoveToConcl  (-1)
                            THEN  GenConclTerm  \mkleeneopen{}s  (1  +  m  +  (d  -  1))\mkleeneclose{}\mcdot{}
                            THEN  Auto))
  )

---

Home Index