---

Step * of Lemma es-bound-list2

∀es:EO
  ∀[T:Type]
    ∀i:Id
      ∀[P:T ─→ ℙ]
        ∀L:T List
          ∀[Q:E ─→ {x:T| (x ∈ L)}  ─→ ℙ]
            ((∀x:T. Dec(P[x]))
            ⇒ (∀x∈L.P[x] ⇒ (∃e:E. Q[e;x]))
               ⇒ ∃e'@i.True supposing ¬(∃x∈L. P[x])
               ⇒ ∃e'@i.(∀x∈L.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x]))) 
               supposing (∀x∈L.∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id))))
BY
{ ((Repeat ((D 0 THENA Complete (Auto)))
    THEN Repeat ((D 0 THENA (Unfolds ``l_all l_exists`` 0 THEN Complete (Auto))))
    THEN AssertBY ⌈L ∈ {x:T| (x ∈ L)}  List⌉ (BLemma `list-set-type` THEN Auto)⋅
    THEN (InstLemma `es-bound-list` [⌈es⌉; ⌈{x:T| (x ∈ L)} ⌉; ⌈i⌉; ⌈P⌉; ⌈Q⌉; ⌈L⌉])⋅)
   THEN Auto
   ) }

---

Latex:


\mforall{}es:EO
    \mforall{}[T:Type]
        \mforall{}i:Id
            \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}]
                \mforall{}L:T  List
                    \mforall{}[Q:E  {}\mrightarrow{}  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}]
                        ((\mforall{}x:T.  Dec(P[x]))
                        {}\mRightarrow{}  (\mforall{}x\mmember{}L.P[x]  {}\mRightarrow{}  (\mexists{}e:E.  Q[e;x]))
                              {}\mRightarrow{}  \mexists{}e'@i.True  supposing  \mneg{}(\mexists{}x\mmember{}L.  P[x])
                              {}\mRightarrow{}  \mexists{}e'@i.(\mforall{}x\mmember{}L.P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x]))) 
                              supposing  (\mforall{}x\mmember{}L.\mforall{}e:E.  (Q[e;x]  {}\mRightarrow{}  (loc(e)  =  i))))


By

((Repeat  ((D  0  THENA  Complete  (Auto)))
    THEN  Repeat  ((D  0  THENA  (Unfolds  ``l\_all  l\_exists``  0  THEN  Complete  (Auto))))
    THEN  AssertBY  \mkleeneopen{}L  \mmember{}  \{x:T|  (x  \mmember{}  L)\}    List\mkleeneclose{}  (BLemma  `list-set-type`  THEN  Auto)\mcdot{}
    THEN  (InstLemma  `es-bound-list`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}\{x:T|  (x  \mmember{}  L)\}  \mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}P\mkleeneclose{};  \mkleeneopen{}Q\mkleeneclose{};  \mkleeneopen{}L\mkleeneclose{}])\mcdot{})
  THEN  Auto
  )

---

Home Index