---

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

.....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)
BY
{ ((HypSubst' (-6) 0 THEN DVar `S0' THEN RepUR ``mapfilter`` 0)
   THEN GenConclAtAddrType ⌈component(P.M[P]) List⌉ [2;2]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....subterm.....  T:t
3:n
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)
11.  x  :  Unit
12.  run-event-local-pred(r;e2)  =  (inr  x  )
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  run-event-loc(e2);fst(S0))
=  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  run-event-loc(e1);fst(S0))


By

---

Latex:
((HypSubst'  (-6)  0  THEN  DVar  `S0'  THEN  RepUR  ``mapfilter``  0)
  THEN  GenConclAtAddrType  \mkleeneopen{}component(P.M[P])  List\mkleeneclose{}  [2;2]\mcdot{}
  THEN  Auto)

---

Home Index