---

Step * of Lemma loc-ordered-filter

∀es:EO. ∀as:E List.  (loc-ordered(es;as) ⇒ (∀P:{e:E| (e ∈ as)}  ─→ 𝔹. loc-ordered(es;filter(P;as))))
BY
{ ((Auto THEN (InstLemma `list-subtype` [⌈E⌉;⌈as⌉]⋅ THENA Auto))
   THEN RepeatFor 3 (ParallelOp -3)
   THEN ParallelLast
   THEN Auto) }

1
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)

---

Latex:


\mforall{}es:EO.  \mforall{}as:E  List.    (loc-ordered(es;as)  {}\mRightarrow{}  (\mforall{}P:\{e:E|  (e  \mmember{}  as)\}    {}\mrightarrow{}  \mBbbB{}.  loc-ordered(es;filter(P;as)))\000C)


By

((Auto  THEN  (InstLemma  `list-subtype`  [\mkleeneopen{}E\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  RepeatFor  3  (ParallelOp  -3)
  THEN  ParallelLast
  THEN  Auto)

---

Home Index