---

Step * of Lemma es-first-at-exists

∀es:EO. ∀i:Id.
  ∀[P:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]
    ((∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e]))
    ⇒ (∀e:E. P[e] ⇒ (∃e':E. (e' ≤loc e  ∧ e' is first@ i s.t.  e.P[e])) supposing loc(e) = i ∈ Id))
BY
{ (RepeatFor 4 ((D 0 THENA Auto)) THEN CausalInd' THEN Auto) }

1
1. es : EO@i'
2. i : Id@i
3. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
4. ∀e:{e:E| loc(e) = i ∈ Id} . Dec(P[e])@i
5. e : E@i
6. ∀e1:E. ((e1 < e) ⇒ P[e1] ⇒ (∃e':E. (e' ≤loc e1  ∧ e' is first@ i s.t.  e.P[e])) supposing loc(e1) = i ∈ Id)
7. loc(e) = i ∈ Id
8. P[e]@i
⊢ ∃e':E. (e' ≤loc e  ∧ e' is first@ i s.t.  e.P[e])

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.
    \mforall{}[P:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}]
        ((\mforall{}e:\{e:E|  loc(e)  =  i\}  .  Dec(P[e]))
        {}\mRightarrow{}  (\mforall{}e:E.  P[e]  {}\mRightarrow{}  (\mexists{}e':E.  (e'  \mleq{}loc  e    \mwedge{}  e'  is  first@  i  s.t.    e.P[e]))  supposing  loc(e)  =  i))


By

(RepeatFor  4  ((D  0  THENA  Auto))  THEN  CausalInd'  THEN  Auto)

---

Home Index