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