Step
*
1
2
1
1
1
of Lemma
eo-strict-forward-before
.....assertion..... 
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
⊢ pred(e) = pred(e) ∈ E
BY
{ (RWO "eo-strict-forward-pred" 0 THEN Auto) }
Latex:
.....assertion..... 
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
\mvdash{}  pred(e)  =  pred(e)
By
(RWO  "eo-strict-forward-pred"  0  THEN  Auto)
Home
Index