---

Step * 1 1 1 1 2 1 of Lemma eo-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) = filter(λa.b ≤loc a;before(e1)) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. loc(e) = loc(b) ∈ Id
8. ¬(e = b ∈ E)
9. before(pred(e)) = filter(λa.b ≤loc a;before(pred(e))) ∈ (E List)
⊢ (before(pred(e)) @ [pred(e)]) = filter(λa.b ≤loc a;before(e)) ∈ (E List)
BY
{ Assert ⌈pred(e) = pred(e) ∈ E⌉⋅ }

1
.....assertion..... 
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. (b ≤loc e1  ⇒ (before(e1) = filter(λa.b ≤loc a;before(e1)) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. loc(e) = loc(b) ∈ Id
8. ¬(e = b ∈ E)
9. before(pred(e)) = filter(λa.b ≤loc a;before(pred(e))) ∈ (E List)
⊢ pred(e) = pred(e) ∈ E

2
1. Info : Type
2. es : EO+(Info)
3. e : E@i
4. ∀e1:E. ((e1 < e) ⇒ (∀b:E. (b ≤loc e1  ⇒ (before(e1) = filter(λa.b ≤loc a;before(e1)) ∈ (E List)))))
5. b : E@i
6. (b <loc e)@i
7. loc(e) = loc(b) ∈ Id
8. ¬(e = b ∈ E)
9. before(pred(e)) = filter(λa.b ≤loc a;before(pred(e))) ∈ (E List)
10. pred(e) = pred(e) ∈ E
⊢ (before(pred(e)) @ [pred(e)]) = filter(λa.b ≤loc a;before(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  \mleq{}loc  e1    {}\mRightarrow{}  (before(e1)  =  filter(\mlambda{}a.b  \mleq{}loc  a;before(e1))))))
5.  b  :  E@i
6.  (b  <loc  e)@i
7.  loc(e)  =  loc(b)
8.  \mneg{}(e  =  b)
9.  before(pred(e))  =  filter(\mlambda{}a.b  \mleq{}loc  a;before(pred(e)))
\mvdash{}  (before(pred(e))  @  [pred(e)])  =  filter(\mlambda{}a.b  \mleq{}loc  a;before(e))


By

Assert  \mkleeneopen{}pred(e)  =  pred(e)\mkleeneclose{}\mcdot{}

---

Home Index