---

Step * of Lemma es-first-at-since-iff

∀es:EO. ∀i:Id. ∀e:E.
  ∀[P,R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ].
    ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)
    ⇒ (es-first-at-since(es;i;e;e.R[e];e.P[e])
       ⇐⇒ (loc(e) = i ∈ Id)
           c∧ ((P[e] ∧ (¬R[e]))
              ∧ ((∃e'':E. ((e'' <loc e) c∧ P[e'']))
                ⇒ (∃e':E
                     ((e' <loc e)
                     c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ ((¬P[e'']) ∧ (¬R[e''])))))))))))
BY
{ (Auto THEN AllHyps h.(Unfold `es-first-at-since` h THEN ExRepD)  THEN Auto) }

1
1. es : EO@i'
2. i : Id@i
3. e : E@i
4. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
5. [R] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
6. ∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id@i
7. loc(e) = i ∈ Id@i
8. P[e]@i
9. ¬R[e]@i
10. ∀e'<e.P[e'] ⇒ (∃e'':E. (e' ≤loc e''  ∧ (e'' <loc e) ∧ R[e'']))@i
11. e'' : E@i
12. (e'' <loc e)@i
13. P[e'']@i
⊢ ∃e':E. ((e' <loc e) c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ ((¬P[e'']) ∧ (¬R[e'']))))))

2
1. es : EO@i'
2. i : Id@i
3. e : E@i
4. [P] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
5. [R] : {e:E| loc(e) = i ∈ Id}  ─→ ℙ
6. ∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id@i
7. (loc(e) = i ∈ Id)
c∧ ((P[e] ∧ (¬R[e]))
   ∧ ((∃e'':E. ((e'' <loc e) c∧ P[e'']))
     ⇒ (∃e':E. ((e' <loc e) c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ ((¬P[e'']) ∧ (¬R[e''])))))))))@i
⊢ es-first-at-since(es;i;e;e.R[e];e.P[e])

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.  \mforall{}e:E.
    \mforall{}[P,R:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}e:E.  Dec(R[e])  supposing  loc(e)  =  i)
        {}\mRightarrow{}  (es-first-at-since(es;i;e;e.R[e];e.P[e])
              \mLeftarrow{}{}\mRightarrow{}  (loc(e)  =  i)
                      c\mwedge{}  ((P[e]  \mwedge{}  (\mneg{}R[e]))
                            \mwedge{}  ((\mexists{}e'':E.  ((e''  <loc  e)  c\mwedge{}  P[e'']))
                                {}\mRightarrow{}  (\mexists{}e':E
                                          ((e'  <loc  e)
                                          c\mwedge{}  (R[e']
                                                \mwedge{}  (\mforall{}e'':E
                                                          ((e'  <loc  e'')  {}\mRightarrow{}  (e''  <loc  e)  {}\mRightarrow{}  ((\mneg{}P[e''])  \mwedge{}  (\mneg{}R[e''])))))))))))


By

(Auto  THEN  AllHyps  h.(Unfold  `es-first-at-since`  h  THEN  ExRepD)    THEN  Auto)

---

Home Index