---

Step * 2 1 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)
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)
BY
{ (Unfold `run-prior-state` 0⋅ THEN OnMaybeHyp 13 (\h. (HypSubst' h 0 THENM (Reduce 0 THEN CompleteAuto)))) }

---

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)
11.  run-event-step(e1)  \mleq{}  run-event-step(e)
12.  run-event-loc(e1)  =  run-event-loc(e)
13.  run-event-local-pred(r;e2)  =  (inl  e)
14.  run-event-interval(r;e1;e2)  =  (run-event-interval(r;e1;e)  @  [e2])
15.  run-event-step(e)  <  run-event-step(e2)
16.  run-event-step(e1)  \mleq{}  run-event-step(e)
17.  run-event-loc(e1)  =  run-event-loc(e)
\mvdash{}  run-prior-state(S0;r;e2)  =  run-event-state(r;e)


By

---

Latex:
(Unfold  `run-prior-state`  0\mcdot{}
  THEN  OnMaybeHyp  13  (\mbackslash{}h.  (HypSubst'  h  0  THENM  (Reduce  0  THEN  CompleteAuto)))
  )

---

Home Index