---

Step * 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. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
10. run-event-local-pred(r;e2) = run-event-local-pred(r;e1) ∈ (runEvents(r)?)
⊢ run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List)
BY
{ (Unfold `run-prior-state` 0⋅ THEN EqCD THEN Try (CompleteAuto)) }

1
.....subterm..... T:t
3:n
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. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
10. run-event-local-pred(r;e2) = run-event-local-pred(r;e1) ∈ (runEvents(r)?)
11. x : Unit
12. run-event-local-pred(r;e2) = (inr x ) ∈ (runEvents(r)?)
⊢ mapfilter(λc.(snd(c));λc.fst(c) = run-event-loc(e2);fst(S0))
= mapfilter(λc.(snd(c));λc.fst(c) = run-event-loc(e1);fst(S0))
∈ (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.  run-event-interval(r;e1;e2)  =  [e2]
10.  run-event-local-pred(r;e2)  =  run-event-local-pred(r;e1)
\mvdash{}  run-prior-state(S0;r;e2)  =  run-prior-state(S0;r;e1)


By

---

Latex:
(Unfold  `run-prior-state`  0\mcdot{}  THEN  EqCD  THEN  Try  (CompleteAuto))

---

Home Index