---

Step * 1 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
⊢ ∀i:ℕm. ∀j:ℕi.  (f j <loc f i)
BY
{ Assert ⌈∀d:ℕ. ∀i:ℕm. ∀j:ℕi.  (((i - j) ≤ d) ⇒ (f j <loc f i))⌉⋅ }

1
.....assertion..... 
1. es : EO@i'
2. m : ℕ+@i
3. f : ℕm ─→ E@i
4. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
⊢ ∀d:ℕ. ∀i:ℕm. ∀j:ℕi.  (((i - j) ≤ d) ⇒ (f j <loc f i))

2
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:ℕ. ∀i:ℕm. ∀j:ℕi.  (((i - j) ≤ d) ⇒ (f j <loc f i))
⊢ ∀i:ℕm. ∀j:ℕi.  (f j <loc f i)

---

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
\mvdash{}  \mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (f  j  <loc  f  i)


By

Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i.    (((i  -  j)  \mleq{}  d)  {}\mRightarrow{}  (f  j  <loc  f  i))\mkleeneclose{}\mcdot{}

---

Home Index