---

Step * 1 1 1 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 ∈ (ℕ × Id)
BY
{ (RepeatFor 2 (DVar `e1')
   THEN RepeatFor 2 (DVar `e2')
   THEN All (RepUR ``run-event-step run-event-loc``)
   THEN EqCD
   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.  run-event-step(e1)  \mleq{}  run-event-step(e2)
7.  run-event-step(e2)  \mleq{}  run-event-step(e1)
\mvdash{}  e1  =  e2


By

---

Latex:
(RepeatFor  2  (DVar  `e1')
  THEN  RepeatFor  2  (DVar  `e2')
  THEN  All  (RepUR  ``run-event-step  run-event-loc``)
  THEN  EqCD
  THEN  Auto)

---

Home Index