---

Step * 3 of Lemma total-run-lt


1. [M] : Type ⟶ Type
2. r : pRunType(P.M[P])@i
3. e1 : runEvents(r)@i
4. e2 : runEvents(r)@i
5. run-event-loc(e1) = run-event-loc(e2) ∈ Id
6. ¬(run-event-step(e1) ≤ run-event-step(e2))
7. run-event-step(e2) ≤ run-event-step(e1)
⊢ (e1 = e2 ∈ runEvents(r)) ∨ (e1 run-pred(r)+ e2) ∨ (e2 run-pred(r)+ e1)
BY
{ (Sel 3 (D 0)
   THEN Auto
   THEN RepUR ``rel_plus`` 0
   THEN (With ⌜1⌝ (D 0)⋅ THENA Auto)
   THEN RWO "rel_exp_one" 0
   THEN Auto
   THEN RepUR ``run-pred infix_ap`` 0
   THEN OrLeft
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])@i
3.  e1  :  runEvents(r)@i
4.  e2  :  runEvents(r)@i
5.  run-event-loc(e1)  =  run-event-loc(e2)
6.  \mneg{}(run-event-step(e1)  \mleq{}  run-event-step(e2))
7.  run-event-step(e2)  \mleq{}  run-event-step(e1)
\mvdash{}  (e1  =  e2)  \mvee{}  (e1  run-pred(r)\msupplus{}  e2)  \mvee{}  (e2  run-pred(r)\msupplus{}  e1)


By

---

Latex:
(Sel  3  (D  0)
  THEN  Auto
  THEN  RepUR  ``rel\_plus``  0
  THEN  (With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THENA  Auto)
  THEN  RWO  "rel\_exp\_one"  0
  THEN  Auto
  THEN  RepUR  ``run-pred  infix\_ap``  0
  THEN  OrLeft
  THEN  Auto)\mcdot{}

---

Home Index