---

Step * 1 of Lemma run-event-cases


1. [M] : Type ─→ Type
2. S0 : System(P.M[P])@i
3. r : pRunType(P.M[P])@i
4. e1 : runEvents(r)@i
5. e2 : runEvents(r)@i
6. run-event-loc(e1) = run-event-loc(e2) ∈ Id
7. run-event-step(e1) ≤ run-event-step(e2)
⊢ ((run-event-local-pred(r;e2) = run-event-local-pred(r;e1) ∈ (runEvents(r)?))
∧ (run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)))
∨ (∃e:runEvents(r)
    (run-event-step(e) < run-event-step(e2)
    ∧ (run-event-step(e1) ≤ run-event-step(e))
    ∧ ((run-event-loc(e1) = run-event-loc(e) ∈ Id) ∧ (run-event-local-pred(r;e2) = (inl e) ∈ (runEvents(r)?)))
    ∧ (run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List))))
BY
{ (RepeatFor 2 (DVar `e2')
   THEN RepeatFor 2 (DVar `e1')
   THEN All
   (RepUR ``run-event-loc run-event-step``)⋅
   THEN All Reduce
   THEN RepUR ``run-event-local-pred run-event-interval
                run-event-history let run-event-step run-event-loc runEvents`` 0⋅
   THEN RenameVar `x' 5
   THEN RenameVar `n' 4
   THEN RenameVar `m' 7
   THEN ((Assert ↑is-run-event(r;m;x) BY (Unhide THEN Auto)) THEN Thin (-4))
   THEN (Assert ↑is-run-event(r;n;x) BY
               (Unhide THEN Auto))
   THEN Thin (-7)
   THEN RevHypSubst' (-4) 0
   THEN ThinVar `e4'⋅) }

1
1. [M] : Type ─→ Type
2. S0 : System(P.M[P])@i
3. r : pRunType(P.M[P])@i
4. n : ℕ@i
5. x : Id@i
6. m : ℕ@i
7. n ≤ m
8. ↑is-run-event(r;m;x)
9. ↑is-run-event(r;n;x)
⊢ ((if null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
then inr ⋅ 
else inl last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
fi 
= if null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n)))
  then inr ⋅ 
  else inl last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n)))
  fi 
∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?))
∧ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m + 1))
  = [<m, x>]
  ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)))
∨ (∃e:{tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
    (fst(e) < m
    ∧ (n ≤ (fst(e)))
    ∧ ((x = (snd(e)) ∈ Id)
      ∧ (if null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
        then inr ⋅ 
        else inl last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
        fi 
        = (inl e)
        ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?)))
    ∧ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m + 1))
      = (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, (fst(e)) + 1)) @ [<m, x>])
      ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List))))

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  S0  :  System(P.M[P])@i
3.  r  :  pRunType(P.M[P])@i
4.  e1  :  runEvents(r)@i
5.  e2  :  runEvents(r)@i
6.  run-event-loc(e1)  =  run-event-loc(e2)
7.  run-event-step(e1)  \mleq{}  run-event-step(e2)
\mvdash{}  ((run-event-local-pred(r;e2)  =  run-event-local-pred(r;e1))  \mwedge{}  (run-event-interval(r;e1;e2)  =  [e2]))
\mvee{}  (\mexists{}e:runEvents(r)
        (run-event-step(e)  <  run-event-step(e2)
        \mwedge{}  (run-event-step(e1)  \mleq{}  run-event-step(e))
        \mwedge{}  ((run-event-loc(e1)  =  run-event-loc(e))  \mwedge{}  (run-event-local-pred(r;e2)  =  (inl  e)))
        \mwedge{}  (run-event-interval(r;e1;e2)  =  (run-event-interval(r;e1;e)  @  [e2]))))


By

---

Latex:
(RepeatFor  2  (DVar  `e2')
  THEN  RepeatFor  2  (DVar  `e1')
  THEN  All
  (RepUR  ``run-event-loc  run-event-step``)\mcdot{}
  THEN  All  Reduce
  THEN  RepUR  ``run-event-local-pred  run-event-interval
                            run-event-history  let  run-event-step  run-event-loc  runEvents``  0\mcdot{}
  THEN  RenameVar  `x'  5
  THEN  RenameVar  `n'  4
  THEN  RenameVar  `m'  7
  THEN  ((Assert  \muparrow{}is-run-event(r;m;x)  BY  (Unhide  THEN  Auto))  THEN  Thin  (-4))
  THEN  (Assert  \muparrow{}is-run-event(r;n;x)  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-7)
  THEN  RevHypSubst'  (-4)  0
  THEN  ThinVar  `e4'\mcdot{})

---

Home Index