---

Step * 1 1 2 2 of Lemma es-increasing-sequence


1. es : EO@i'
2. m : ℕ+@i
3. f : ℕm ─→ E@i
4. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
5. d : ℤ
6. 0 < d
7. ∀i:ℕm. ∀j:ℕi.  (((i - j) ≤ (d - 1)) ⇒ (f j <loc f i))
8. i : ℕm@i
9. j : ℕi@i
10. (i - j) ≤ d@i
11. (f j <loc f (j + 1))
12. ¬(i = (j + 1) ∈ ℤ)
⊢ (f j <loc f i)
BY
{ ((InstHyp [⌈i⌉; ⌈j + 1⌉] (-6))⋅ THEN Auto' THEN (InstLemma `es-locl-trans` []) THEN UseTrans ⌈f (j + 1)⌉⋅) }

---

Latex:



1.  es  :  EO@i'
2.  m  :  \mBbbN{}\msupplus{}@i
3.  f  :  \mBbbN{}m  {}\mrightarrow{}  E@i
4.  \mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1))@i
5.  d  :  \mBbbZ{}
6.  0  <  d
7.  \mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (((i  -  j)  \mleq{}  (d  -  1))  {}\mRightarrow{}  (f  j  <loc  f  i))
8.  i  :  \mBbbN{}m@i
9.  j  :  \mBbbN{}i@i
10.  (i  -  j)  \mleq{}  d@i
11.  (f  j  <loc  f  (j  +  1))
12.  \mneg{}(i  =  (j  +  1))
\mvdash{}  (f  j  <loc  f  i)


By

((InstHyp  [\mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}j  +  1\mkleeneclose{}]  (-6))\mcdot{}
  THEN  Auto'
  THEN  (InstLemma  `es-locl-trans`  [])
  THEN  UseTrans  \mkleeneopen{}f  (j  +  1)\mkleeneclose{}\mcdot{})

---

Home Index