---

Step * of Lemma es-increasing-sequence2

∀es:EO. ∀m:ℕ+. ∀f:ℕm ⟶ E.  ((∀i:ℕm - 1. (f i <loc f (i + 1))) ⇒ (∀i:ℕm. ∀j:ℕi + 1.  f j ≤loc f i ))
BY
{ ((((Auto THEN (InstLemma `es-increasing-sequence` [⌜es⌝; ⌜m⌝; ⌜f⌝])⋅) THENA Auto) THEN Decide ⌜i = j ∈ ℤ⌝⋅)
   THENA Auto
   ) }

1
1. es : EO@i'
2. m : ℕ+@i
3. f : ℕm ⟶ E@i
4. ∀i:ℕm - 1. (f i <loc f (i + 1))@i
5. i : ℕm@i
6. j : ℕi + 1@i
7. ∀i:ℕm. ∀j:ℕi.  (f j <loc f i)
8. i = j ∈ ℤ
⊢ 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. i : ℕm@i
6. j : ℕi + 1@i
7. ∀i:ℕm. ∀j:ℕi.  (f j <loc f i)
8. ¬(i = j ∈ ℤ)
⊢ f j ≤loc f i 

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}m:\mBbbN{}\msupplus{}.  \mforall{}f:\mBbbN{}m  {}\mrightarrow{}  E.
    ((\mforall{}i:\mBbbN{}m  -  1.  (f  i  <loc  f  (i  +  1)))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}m.  \mforall{}j:\mBbbN{}i  +  1.    f  j  \mleq{}loc  f  i  ))


By

---

Latex:
((((Auto  THEN  (InstLemma  `es-increasing-sequence`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}m\mkleeneclose{};  \mkleeneopen{}f\mkleeneclose{}])\mcdot{})  THENA  Auto)
    THEN  Decide  \mkleeneopen{}i  =  j\mkleeneclose{}\mcdot{}
    )
  THENA  Auto
  )

---

Home Index