---

Step * 1 1 1 of Lemma es-bound-list


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∈[u / v].∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id)))
10. (∀x∈[u / v].P[x] ⇒ (∃e:E. Q[e;x]))@i
11. ∃e'@i.True supposing ¬(∃x∈[u / v]. P[x])@i
12. ∃e'@i.True supposing ¬(∃x∈v. P[x]) ⇒ ∃e'@i.(∀x∈v.P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))
13. P[u]
⊢ ∃e'@i.(∀x∈[u / v].P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))
BY
{ ((((AssertBY ⌈∃e:E. Q[e;u]⌉
       AllHyps h.((RWO "l_all_iff" h THENA Auto) THEN BHyp h THEN Auto THEN ProveListMember THEN Auto') )⋅
     THEN ExRepD
     THEN (AssertBY ⌈loc(e) = i ∈ Id⌉ AllHyps h.((RWO "l_all_iff" h THENA Auto)
                                                 THEN (InstHyp [⌈u⌉; ⌈e⌉] h)⋅
                                                 THEN Auto
                                                 THEN ProveListMember
                                                 THEN Auto') )⋅
     THEN (D (-5)))
    THENA (Auto THEN Unfold `existse-at` 0 THEN (InstConcl [⌈e⌉])⋅ THEN Auto)
    )
   THEN (All (Unfolds ``existse-at``))
   THEN (All (RWO "l_all_iff")⋅ THENA 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:T. ((x ∈ [u / v]) ⇒ (∀e:E. (Q[e;x] ⇒ (loc(e) = i ∈ Id))))
10. ∀x:T. ((x ∈ [u / v]) ⇒ P[x] ⇒ (∃e:E. Q[e;x]))
11. ∃e':E. ((loc(e') = i ∈ Id) ∧ True) supposing ¬(∃x∈[u / v]. P[x])@i
12. P[u]
13. e : E
14. Q[e;u]
15. loc(e) = i ∈ Id
16. ∃e':E. ((loc(e') = i ∈ Id) ∧ (∀x:T. ((x ∈ v) ⇒ P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))))
⊢ ∃e':E. ((loc(e') = i ∈ Id) ∧ (∀x:T. ((x ∈ [u / v]) ⇒ P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))))

---

Latex:



1.  es  :  EO@i'
2.  [T]  :  Type
3.  i  :  Id@i
4.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
5.  [Q]  :  E  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
6.  \mforall{}x:T.  Dec(P[x])@i
7.  u  :  T@i
8.  v  :  T  List@i
9.  (\mforall{}x\mmember{}[u  /  v].\mforall{}e:E.  (Q[e;x]  {}\mRightarrow{}  (loc(e)  =  i)))
10.  (\mforall{}x\mmember{}[u  /  v].P[x]  {}\mRightarrow{}  (\mexists{}e:E.  Q[e;x]))@i
11.  \mexists{}e'@i.True  supposing  \mneg{}(\mexists{}x\mmember{}[u  /  v].  P[x])@i
12.  \mexists{}e'@i.True  supposing  \mneg{}(\mexists{}x\mmember{}v.  P[x])  {}\mRightarrow{}  \mexists{}e'@i.(\mforall{}x\mmember{}v.P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x])))
13.  P[u]
\mvdash{}  \mexists{}e'@i.(\mforall{}x\mmember{}[u  /  v].P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x])))


By

((((AssertBY  \mkleeneopen{}\mexists{}e:E.  Q[e;u]\mkleeneclose{}
          AllHyps  h.((RWO  "l\_all\_iff"  h  THENA  Auto)
                                THEN  BHyp  h
                                THEN  Auto
                                THEN  ProveListMember
                                THEN  Auto')  )\mcdot{}
      THEN  ExRepD
      THEN  (AssertBY  \mkleeneopen{}loc(e)  =  i\mkleeneclose{}  AllHyps  h.((RWO  "l\_all\_iff"  h  THENA  Auto)
                                                                                    THEN  (InstHyp  [\mkleeneopen{}u\mkleeneclose{};  \mkleeneopen{}e\mkleeneclose{}]  h)\mcdot{}
                                                                                    THEN  Auto
                                                                                    THEN  ProveListMember
                                                                                    THEN  Auto')  )\mcdot{}
      THEN  (D  (-5)))
    THENA  (Auto  THEN  Unfold  `existse-at`  0  THEN  (InstConcl  [\mkleeneopen{}e\mkleeneclose{}])\mcdot{}  THEN  Auto)
    )
  THEN  (All  (Unfolds  ``existse-at``))
  THEN  (All  (RWO  "l\_all\_iff")\mcdot{}  THENA  Auto))\mcdot{}

---

Home Index