---

Step * 1 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: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])))))
BY
{ (ExRepD THEN Assert ⌈e ≤loc e'  ∨ e' ≤loc e ⌉⋅) }

1
.....assertion..... 
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])))
⊢ e ≤loc e'  ∨ e' ≤loc e 

2
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])))))

---

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.  \mexists{}e':E.  ((loc(e')  =  i)  \mwedge{}  (\mforall{}x:T.  ((x  \mmember{}  v)  {}\mRightarrow{}  P[x]  {}\mRightarrow{}  (\mexists{}e:E.  (e  \mleq{}loc  e'    \mwedge{}  Q[e;x])))))
\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

(ExRepD  THEN  Assert  \mkleeneopen{}e  \mleq{}loc  e'    \mvee{}  e'  \mleq{}loc  e  \mkleeneclose{}\mcdot{})

---

Home Index