---

Step * of Lemma l-ordered-from-upto-lt

∀[n,m:ℤ].  l-ordered(ℤ;x,y.x < y;[n, m))
BY
{ (Auto
   THEN (Decide ⌜m ≤ n⌝⋅ THENA Auto)
   THEN Try (((RWO "from-upto-is-nil<" (-1) THENA Auto) THEN RWO "-1" 0 THEN RW ListC 0 THEN Auto))
   THEN (Assert ⌜∃k:ℕ. (m = (n + k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto))
   THEN ExRepD
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN ThinVar `m'
   THEN MoveToConcl (-2)
   THEN NatInd (-1)
   THEN Auto
   THEN Try (Complete ((RWO "from-upto-nil" 0 THEN Auto THEN RW ListC 0 THEN Auto)))
   THEN (RWO "from-upto-decomp-last" 0 THENA Auto)
   THEN RWO "l-ordered-append" 0
   THEN Auto
   THEN Try (Complete ((Subst ⌜(n + k) - 1 ~ n + (k - 1)⌝ 0⋅ THEN Auto)))
   THEN Try (Complete ((BLemma `l-ordered-single` THEN Auto)))
   THEN All(RW ListC)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n,m:\mBbbZ{}].    l-ordered(\mBbbZ{};x,y.x  <  y;[n,  m))


By

---

Latex:
(Auto
  THEN  (Decide  \mkleeneopen{}m  \mleq{}  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((RWO  "from-upto-is-nil<"  (-1)  THENA  Auto)  THEN  RWO  "-1"  0  THEN  RW  ListC  0  THEN  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  THENA  Auto)
  THEN  ThinVar  `m'
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1)
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "from-upto-nil"  0  THEN  Auto  THEN  RW  ListC  0  THEN  Auto)))
  THEN  (RWO  "from-upto-decomp-last"  0  THENA  Auto)
  THEN  RWO  "l-ordered-append"  0
  THEN  Auto
  THEN  Try  (Complete  ((Subst  \mkleeneopen{}(n  +  k)  -  1  \msim{}  n  +  (k  -  1)\mkleeneclose{}  0\mcdot{}  THEN  Auto)))
  THEN  Try  (Complete  ((BLemma  `l-ordered-single`  THEN  Auto)))
  THEN  All(RW  ListC)
  THEN  Auto)

---

Home Index