---

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


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 
BY
{ (CaseNat 0 `i' THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  n  :  \mBbbN{}\msupplus{}@i
3.  f  :  \mBbbN{}1  {}\mrightarrow{}  E@i
4.  \mforall{}i,j:\mBbbN{}1.    (loc(f  i)  =  loc(f  j))
5.  i  :  \mBbbN{}1@i
\mvdash{}  f  i  \mleq{}loc  f  0 


By

(CaseNat  0  `i'  THEN  Auto)

---

Home Index