---

Step * of Lemma from-upto-decomp-last

∀[n,m:ℤ].  [n, m) = ([n, m - 1) @ [m - 1]) ∈ (ℤ List) supposing n < m
BY
{ (Auto
   THEN (Assert ⌜∃k:ℕ. (m = (n + k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
   THEN ExRepD
   THEN HypSubst' (-1) 0
   THEN (HypSubst' (-1) (-3) THENA Auto)
   THEN (Assert ⌜0 < k⌝⋅ THENA Auto')
   THEN ThinVar `m'
   THEN Thin (-2)
   THEN MoveToConcl 1
   THEN NatInd (-2)
   THEN Auto) }

1
1. k : ℤ
2. 0 < k
3. 0 < k - 1 ⇒ (∀n:ℤ. ([n, n + (k - 1)) = ([n, (n + (k - 1)) - 1) @ [(n + (k - 1)) - 1]) ∈ (ℤ List)))
4. 0 < k
5. n : ℤ
⊢ [n, n + k) = ([n, (n + k) - 1) @ [(n + k) - 1]) ∈ (ℤ List)

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].    [n,  m)  =  ([n,  m  -  1)  @  [m  -  1])  supposing  n  <  m


By

---

Latex:
(Auto
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (m  =  (n  +  k))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  (HypSubst'  (-1)  (-3)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}0  <  k\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  ThinVar  `m'
  THEN  Thin  (-2)
  THEN  MoveToConcl  1
  THEN  NatInd  (-2)
  THEN  Auto)

---

Home Index