---

Step * 1 2 1 1 2 1 of Lemma eo-strict-forward-before


1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. ((b <loc e1) ⇒ (before(e1) = (b, e1) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. e ∈ E
8. loc(e) = loc(b) ∈ Id
9. ¬↑first(e)
10. ¬(pred(e) = b ∈ E)
11. before(pred(e)) = (b, pred(e)) ∈ (E List)
12. pred(e) ∈ E
13. ¬↑first(e)
14. E ⊆r E
15. pred(e) = pred(e) ∈ E
16. pred(e) = pred(e) ∈ E
⊢ ((b, pred(e)) @ [pred(e)]) = (b, e) ∈ (E List)
BY
{ (Unfold `es-open-interval` 0
   THEN (InstLemma `es-before-partition` [⌈es⌉;⌈e⌉;⌈pred(e)⌉]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Unfold `es-le-before` 0
   THEN RepeatFor 2 ((RWO "filter_append_sq" 0 THENA Auto))
   THEN Reduce 0
   THEN AutoSplit) }

1
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. ((b <loc e1) ⇒ (before(e1) = (b, e1) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. e ∈ E
8. loc(e) = loc(b) ∈ Id
9. ¬↑first(e)
10. ¬(pred(e) = b ∈ E)
11. before(pred(e)) = (b, pred(e)) ∈ (E List)
12. pred(e) ∈ E
13. ¬↑first(e)
14. E ⊆r E
15. pred(e) = pred(e) ∈ E
16. pred(e) = pred(e) ∈ E
17. before(e) = (≤loc(pred(e)) @ (pred(e), e)) ∈ (E List)
18. (b <loc pred(e))
⊢ (filter(λev.b <loc ev;before(pred(e))) @ [pred(e)])
= ((filter(λev.b <loc ev;before(pred(e))) @ [pred(e)]) @ filter(λev.b <loc ev;(pred(e), e)))
∈ (E List)

2
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. ((b <loc e1) ⇒ (before(e1) = (b, e1) ∈ (E List)))))
5. b : E@i
6. ¬(b <loc pred(e))
7. (b <loc e)@i
8. e ∈ E
9. loc(e) = loc(b) ∈ Id
10. ¬↑first(e)
11. ¬(pred(e) = b ∈ E)
12. before(pred(e)) = (b, pred(e)) ∈ (E List)
13. pred(e) ∈ E
14. ¬↑first(e)
15. E ⊆r E
16. pred(e) = pred(e) ∈ E
17. pred(e) = pred(e) ∈ E
18. before(e) = (≤loc(pred(e)) @ (pred(e), e)) ∈ (E List)
⊢ (filter(λev.b <loc ev;before(pred(e))) @ [pred(e)])
= ((filter(λev.b <loc ev;before(pred(e))) @ []) @ filter(λev.b <loc ev;(pred(e), e)))
∈ (E List)

---

Latex:



1.  Info  :  Type
2.  es  :  EO+(Info)
3.  e  :  E@i
4.  \mforall{}e1:E.  ((e1  <  e)  {}\mRightarrow{}  (\mforall{}b:E.  ((b  <loc  e1)  {}\mRightarrow{}  (before(e1)  =  (b,  e1)))))
5.  b  :  E@i
6.  (b  <loc  e)@i
7.  e  \mmember{}  E
8.  loc(e)  =  loc(b)
9.  \mneg{}\muparrow{}first(e)
10.  \mneg{}(pred(e)  =  b)
11.  before(pred(e))  =  (b,  pred(e))
12.  pred(e)  \mmember{}  E
13.  \mneg{}\muparrow{}first(e)
14.  E  \msubseteq{}r  E
15.  pred(e)  =  pred(e)
16.  pred(e)  =  pred(e)
\mvdash{}  ((b,  pred(e))  @  [pred(e)])  =  (b,  e)


By

(Unfold  `es-open-interval`  0
  THEN  (InstLemma  `es-before-partition`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}pred(e)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Unfold  `es-le-before`  0
  THEN  RepeatFor  2  ((RWO  "filter\_append\_sq"  0  THENA  Auto))
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index