---

Step * 2 of Lemma run-event-interval-cases


1. [M] : Type ─→ Type
2. S0 : System(P.M[P])@i
3. r : fulpRunType(P.M[P])@i
4. r ∈ pRunType(P.M[P])
5. e1 : runEvents(r)@i
6. e2 : runEvents(r)@i
7. run-event-loc(e1) = run-event-loc(e2) ∈ Id
8. run-event-step(e1) ≤ run-event-step(e2)
9. e : runEvents(r)
10. run-event-step(e) < run-event-step(e2)
∧ (run-event-step(e1) ≤ run-event-step(e))
∧ ((run-event-loc(e1) = run-event-loc(e) ∈ Id) ∧ (run-event-local-pred(r;e2) = (inl e) ∈ (runEvents(r)?)))
∧ (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List))
⊢ run-event-step(e) < run-event-step(e2)
∧ (run-event-step(e1) ≤ run-event-step(e))
∧ ((run-event-loc(e1) = run-event-loc(e) ∈ Id)
  ∧ (run-prior-state(S0;r;e2) = run-event-state(r;e) ∈ (Process(P.M[P]) List)))
∧ (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List))
BY
{ Auto }

1
1. M : Type ─→ Type
2. S0 : System(P.M[P])@i
3. r : fulpRunType(P.M[P])@i
4. r ∈ pRunType(P.M[P])
5. e1 : runEvents(r)@i
6. e2 : runEvents(r)@i
7. run-event-loc(e1) = run-event-loc(e2) ∈ Id
8. run-event-step(e1) ≤ run-event-step(e2)
9. e : runEvents(r)
10. run-event-step(e) < run-event-step(e2)
11. run-event-step(e1) ≤ run-event-step(e)
12. run-event-loc(e1) = run-event-loc(e) ∈ Id
13. run-event-local-pred(r;e2) = (inl e) ∈ (runEvents(r)?)
14. run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List)
15. run-event-step(e) < run-event-step(e2)
16. run-event-step(e1) ≤ run-event-step(e)
17. run-event-loc(e1) = run-event-loc(e) ∈ Id
⊢ run-prior-state(S0;r;e2) = run-event-state(r;e) ∈ (Process(P.M[P]) List)

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  S0  :  System(P.M[P])@i
3.  r  :  fulpRunType(P.M[P])@i
4.  r  \mmember{}  pRunType(P.M[P])
5.  e1  :  runEvents(r)@i
6.  e2  :  runEvents(r)@i
7.  run-event-loc(e1)  =  run-event-loc(e2)
8.  run-event-step(e1)  \mleq{}  run-event-step(e2)
9.  e  :  runEvents(r)
10.  run-event-step(e)  <  run-event-step(e2)
\mwedge{}  (run-event-step(e1)  \mleq{}  run-event-step(e))
\mwedge{}  ((run-event-loc(e1)  =  run-event-loc(e))  \mwedge{}  (run-event-local-pred(r;e2)  =  (inl  e)))
\mwedge{}  (run-event-interval(r;e1;e2)  =  (run-event-interval(r;e1;e)  @  [e2]))
\mvdash{}  run-event-step(e)  <  run-event-step(e2)
\mwedge{}  (run-event-step(e1)  \mleq{}  run-event-step(e))
\mwedge{}  ((run-event-loc(e1)  =  run-event-loc(e))  \mwedge{}  (run-prior-state(S0;r;e2)  =  run-event-state(r;e)))
\mwedge{}  (run-event-interval(r;e1;e2)  =  (run-event-interval(r;e1;e)  @  [e2]))


By

---

Latex:
Auto

---

Home Index