---

Step * 1 of Lemma last-event


1. ∀es:EO. ∀i:Id.
     ∀[R:{e:E| loc(e) = i ∈ Id}  ─→ ℙ]
       ∀e:E
         ((∀e:E. Dec(R[e]) supposing loc(e) = i ∈ Id)
         ⇒ (∃e':E. (e' ≤loc e  c∧ R[e']))
            ⇒ (∃e':E. (e' ≤loc e  c∧ (R[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬R[e''])))))) 
            supposing loc(e) = i ∈ Id)
⊢ ∀es:EO. ∀e:E.
    ∀[P:{a:E| loc(a) = loc(e) ∈ Id}  ─→ ℙ]
      ((∀a:{a:E| loc(a) = loc(e) ∈ Id} . Dec(P[a]))
      ⇒ (∀e'≤e.¬P[e'] ∨ (∃e':E. (e' ≤loc e  c∧ (P[e'] ∧ (∀e'':E. ((e' <loc e'') ⇒ e'' ≤loc e  ⇒ (¬P[e'']))))))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert Dec(∃e':E. (e' ≤loc e  c∧ P[e'])) BY
               (Fold `existse-le` 0 THEN BLemma `decidable__existse-le` THEN Auto THEN D 0 THEN Auto))
   ) }

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

---

Latex:



1.  \mforall{}es:EO.  \mforall{}i:Id.
          \mforall{}[R:\{e:E|  loc(e)  =  i\}    {}\mrightarrow{}  \mBbbP{}]
              \mforall{}e:E
                  ((\mforall{}e:E.  Dec(R[e])  supposing  loc(e)  =  i)
                  {}\mRightarrow{}  (\mexists{}e':E.  (e'  \mleq{}loc  e    c\mwedge{}  R[e']))
                        {}\mRightarrow{}  (\mexists{}e':E
                                  (e'  \mleq{}loc  e    c\mwedge{}  (R[e']  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}R[e''])))))) 
                        supposing  loc(e)  =  i)
\mvdash{}  \mforall{}es:EO.  \mforall{}e:E.
        \mforall{}[P:\{a:E|  loc(a)  =  loc(e)\}    {}\mrightarrow{}  \mBbbP{}]
            ((\mforall{}a:\{a:E|  loc(a)  =  loc(e)\}  .  Dec(P[a]))
            {}\mRightarrow{}  (\mforall{}e'\mleq{}e.\mneg{}P[e']
                  \mvee{}  (\mexists{}e':E
                          (e'  \mleq{}loc  e    c\mwedge{}  (P[e']  \mwedge{}  (\mforall{}e'':E.  ((e'  <loc  e'')  {}\mRightarrow{}  e''  \mleq{}loc  e    {}\mRightarrow{}  (\mneg{}P[e'']))))))))


By

((UnivCD  THENA  Auto)
  THEN  (Assert  Dec(\mexists{}e':E.  (e'  \mleq{}loc  e    c\mwedge{}  P[e']))  BY
                          (Fold  `existse-le`  0  THEN  BLemma  `decidable\_\_existse-le`  THEN  Auto  THEN  D  0  THEN  Auto))
  )

---

Home Index