---

Step * 1 of Lemma loc-ordered-filter


1. es : EO@i'
2. as : E List@i
3. ∀x,y:E.  (x before y ∈ as ⇒ (x <loc y))@i
4. P : {e:E| (e ∈ as)}  ─→ 𝔹@i
5. as ∈ {a:E| (a ∈ as)}  List
6. x : E@i
7. ∀y:E. (x before y ∈ as ⇒ (x <loc y))
8. y : E@i
9. x before y ∈ as ⇒ (x <loc y)
10. x before y ∈ filter(P;as)@i
⊢ (x <loc y)
BY
{ (D (-2) THEN Auto) }

1
.....antecedent..... 
1. es : EO@i'
2. as : E List@i
3. ∀x,y:E.  (x before y ∈ as ⇒ (x <loc y))@i
4. P : {e:E| (e ∈ as)}  ─→ 𝔹@i
5. as ∈ {a:E| (a ∈ as)}  List
6. x : E@i
7. ∀y:E. (x before y ∈ as ⇒ (x <loc y))
8. y : E@i
9. x before y ∈ filter(P;as)@i
⊢ x before y ∈ as

---

Latex:



1.  es  :  EO@i'
2.  as  :  E  List@i
3.  \mforall{}x,y:E.    (x  before  y  \mmember{}  as  {}\mRightarrow{}  (x  <loc  y))@i
4.  P  :  \{e:E|  (e  \mmember{}  as)\}    {}\mrightarrow{}  \mBbbB{}@i
5.  as  \mmember{}  \{a:E|  (a  \mmember{}  as)\}    List
6.  x  :  E@i
7.  \mforall{}y:E.  (x  before  y  \mmember{}  as  {}\mRightarrow{}  (x  <loc  y))
8.  y  :  E@i
9.  x  before  y  \mmember{}  as  {}\mRightarrow{}  (x  <loc  y)
10.  x  before  y  \mmember{}  filter(P;as)@i
\mvdash{}  (x  <loc  y)


By

(D  (-2)  THEN  Auto)

---

Home Index