---

Step * 1 of Lemma last-event-of-set

.....basecase..... 
1. es : EO@i'
2. n : ℕ+@i
⊢ ∀f:ℕ1 ─→ E. ∃k:ℕ1. ∀i:ℕ1. f i ≤loc f k  supposing ∀i,j:ℕ1.  (loc(f i) = loc(f j) ∈ Id)
BY
{ (Auto THEN With ⌈0⌉ (D 0)⋅ THEN Auto) }

1
1. es : EO@i'
2. n : ℕ+@i
3. f : ℕ1 ─→ E@i
4. ∀i,j:ℕ1.  (loc(f i) = loc(f j) ∈ Id)
5. i : ℕ1@i
⊢ f i ≤loc f 0 

---

Latex:


.....basecase..... 
1.  es  :  EO@i'
2.  n  :  \mBbbN{}\msupplus{}@i
\mvdash{}  \mforall{}f:\mBbbN{}1  {}\mrightarrow{}  E.  \mexists{}k:\mBbbN{}1.  \mforall{}i:\mBbbN{}1.  f  i  \mleq{}loc  f  k    supposing  \mforall{}i,j:\mBbbN{}1.    (loc(f  i)  =  loc(f  j))


By

(Auto  THEN  With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index