---

Step * of Lemma es-bound-list

∀es:EO
  ∀[T:Type]
    ∀i:Id
      ∀[P:T ─→ ℙ]. ∀[Q:E ─→ T ─→ ℙ].
        ((∀x:T. Dec(P[x]))
        ⇒ (∀L:T List
              (∀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
{ (InductionOnList
   THEN Auto
   THEN (RWW "l_exists_nil" (-1))
   THEN Auto
   THEN Try ((RepeatFor 2 (ParallelLast) THEN Auto))) }

1
1. es : EO@i'
2. [T] : Type
3. i : Id@i
4. [P] : T ─→ ℙ
5. [Q] : E ─→ T ─→ ℙ
6. ∀x:T. Dec(P[x])@i
7. u : T@i
8. v : T List@i
9. (∀x∈v.P[x] ⇒ (∃e:E. Q[e;x]))
   ⇒ ∃e'@i.True supposing ¬(∃x∈v. P[x])
   ⇒ ∃e'@i.(∀x∈v.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x]))) 
   supposing (∀x∈v.∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))@i
10. (∀x∈[u / v].∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))
11. (∀x∈[u / v].P[x] ⇒ (∃e:E. Q[e;x]))@i
12. ∃e'@i.True supposing ¬(∃x∈[u / v]. P[x])@i
⊢ ∃e'@i.(∀x∈[u / v].P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))

---

Latex:


\mforall{}es:EO
    \mforall{}[T:Type]
        \mforall{}i:Id
            \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q:E  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
                ((\mforall{}x:T.  Dec(P[x]))
                {}\mRightarrow{}  (\mforall{}L:T  List
                            (\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

(InductionOnList
  THEN  Auto
  THEN  (RWW  "l\_exists\_nil"  (-1))
  THEN  Auto
  THEN  Try  ((RepeatFor  2  (ParallelLast)  THEN  Auto)))

---

Home Index