---

Step * 1 1 1 1 2 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: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
17. loc(e') = i ∈ Id
18. ∀x:T. ((x ∈ v) ⇒ P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))
19. e ≤loc e'  ∨ e' ≤loc e 
⊢ ∃e':E. ((loc(e') = i ∈ Id) ∧ (∀x:T. ((x ∈ [u / v]) ⇒ P[x] ⇒ (∃e:E. (e ≤loc e'  ∧ Q[e;x])))))
BY
{ (((((D (-1)) THENL [(InstConcl [⌈e'⌉])⋅; (InstConcl [⌈e⌉])⋅]) THEN Auto THEN (RWO "cons_member" (-2))) THENM (D (-2)))
   THEN Auto
   THEN Try ((((HypSubst (-2) 0) THENA Auto)
              THEN (InstConcl [⌈e⌉])⋅
              THEN Auto
              THEN Unfold `es-le` 0
              THEN OrRight
              THEN Auto))
   THEN OnMaybeHyp 19 (\h. ((InstHyp [⌈x⌉] h)⋅
                            THEN Auto
                            THEN RepeatFor 2 (ParallelLast)
                            THEN ((InstLemma `es-le-trans` [⌈es⌉])⋅ THENA Auto)
                            THEN UseTrans ⌈e'⌉⋅))) }

---

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:T.  ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  (\mforall{}e:E.  (Q[e;x]  {}\mRightarrow{}  (loc(e)  =  i))))
10.  \mforall{}x:T.  ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  (\mexists{}e:E.  Q[e;x]))
11.  \mexists{}e':E.  ((loc(e')  =  i)  \mwedge{}  True)  supposing  \mneg{}(\mexists{}x\mmember{}[u  /  v].  P[x])@i
12.  P[u]
13.  e  :  E
14.  Q[e;u]
15.  loc(e)  =  i
16.  e'  :  E
17.  loc(e')  =  i
18.  \mforall{}x:T.  ((x  \mmember{}  v)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x])))
19.  e  \mleq{}loc  e'    \mvee{}  e'  \mleq{}loc  e 
\mvdash{}  \mexists{}e':E.  ((loc(e')  =  i)  \mwedge{}  (\mforall{}x:T.  ((x  \mmember{}  [u  /  v])  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x])))))


By

(((((D  (-1))  THENL  [(InstConcl  [\mkleeneopen{}e'\mkleeneclose{}])\mcdot{};  (InstConcl  [\mkleeneopen{}e\mkleeneclose{}])\mcdot{}])
      THEN  Auto
      THEN  (RWO  "cons\_member"  (-2)))
  THENM  (D  (-2))
  )
  THEN  Auto
  THEN  Try  ((((HypSubst  (-2)  0)  THENA  Auto)
                        THEN  (InstConcl  [\mkleeneopen{}e\mkleeneclose{}])\mcdot{}
                        THEN  Auto
                        THEN  Unfold  `es-le`  0
                        THEN  OrRight
                        THEN  Auto))
  THEN  OnMaybeHyp  19  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  h)\mcdot{}
                                                    THEN  Auto
                                                    THEN  RepeatFor  2  (ParallelLast)
                                                    THEN  ((InstLemma  `es-le-trans`  [\mkleeneopen{}es\mkleeneclose{}])\mcdot{}  THENA  Auto)
                                                    THEN  UseTrans  \mkleeneopen{}e'\mkleeneclose{}\mcdot{})))

---

Home Index