---

Step * 1 1 1 of Lemma stdEO-event-history


1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : {e:runEvents(r)| True} @i
4. e2 : {e:runEvents(r)| True} @i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
6. run-event-step(e1) < run-event-step(e2)@i
⊢ (e1 ∈ mapfilter(λt.<t, run-event-loc(e2)>;λt.is-run-event(r;t;run-event-loc(e2));[0, run-event-step(e2))))
BY
{ (RWO "member-mapfilter" 0
   THEN All Reduce
   THEN Auto
   THEN Try ((D -1 THEN MemTypeCD THEN Auto))
   THEN With ⌈run-event-step(e1)⌉ (D 0)⋅
   THEN Auto
   THEN Auto')⋅ }

1
1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : {e:runEvents(r)| True} @i
4. e2 : {e:runEvents(r)| True} @i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
6. run-event-step(e1) < run-event-step(e2)@i
7. (run-event-step(e1) ∈ [0, run-event-step(e2)))
⊢ ↑is-run-event(r;run-event-step(e1);run-event-loc(e2))

2
1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : {e:runEvents(r)| True} @i
4. e2 : {e:runEvents(r)| True} @i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
6. run-event-step(e1) < run-event-step(e2)@i
7. (run-event-step(e1) ∈ [0, run-event-step(e2)))
8. ↑is-run-event(r;run-event-step(e1);run-event-loc(e2))
⊢ e1 = <run-event-step(e1), run-event-loc(e2)> ∈ runEvents(r)

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
3.  e1  :  \{e:runEvents(r)|  True\}  @i
4.  e2  :  \{e:runEvents(r)|  True\}  @i
5.  run-event-loc(e1)  =  run-event-loc(e2)@i
6.  run-event-step(e1)  <  run-event-step(e2)@i
\mvdash{}  (e1  \mmember{}  mapfilter(\mlambda{}t.<t,  run-event-loc(e2)>
                                    \mlambda{}t.is-run-event(r;t;run-event-loc(e2));
                                    [0,  run-event-step(e2))))


By

---

Latex:
(RWO  "member-mapfilter"  0
  THEN  All  Reduce
  THEN  Auto
  THEN  Try  ((D  -1  THEN  MemTypeCD  THEN  Auto))
  THEN  With  \mkleeneopen{}run-event-step(e1)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  Auto')\mcdot{}

---

Home Index