---

Step * of Lemma es-first-at-exists-cases

∀es:EO. ∀e:E.
  ∀[P:{e':E| loc(e') = loc(e) ∈ Id}  ─→ ℙ]
    ((∀e':{e':E| loc(e') = loc(e) ∈ Id} . Dec(P[e']))
    ⇒ ((∀e'≤e.¬P[e'] ∧ (¬∃e'≤e.e' is first@ loc(e) s.t.  e'.P[e']))
       ∨ ((¬∀e'≤e.¬P[e']) ∧ ∃e'≤e.e' is first@ loc(e) s.t.  e'.P[e'])))
BY
{ (Auto
   THEN (Assert Dec(∀e'≤e.¬P[e']) BY
               (ProveDecidable1 THEN Auto THEN D 0 THEN Auto))
   THEN Unfold `decidable` -1
   THEN ParallelLast
   THEN Auto
   THEN Thin (-1)
   THEN Try ((BLemma `es-first-at-exists2`  THEN Auto))) }

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

---

Latex:


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


By

(Auto
  THEN  (Assert  Dec(\mforall{}e'\mleq{}e.\mneg{}P[e'])  BY
                          (ProveDecidable1  THEN  Auto  THEN  D  0  THEN  Auto))
  THEN  Unfold  `decidable`  -1
  THEN  ParallelLast
  THEN  Auto
  THEN  Thin  (-1)
  THEN  Try  ((BLemma  `es-first-at-exists2`    THEN  Auto)))

---

Home Index