---

Step * 8 of Lemma run-eo_wf


1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
4. ∀x,y:runEvents(r).  ((↓x run-lt(r) y) ⇒ run-event-step(x) < run-event-step(y))
5. ∀e:runEvents(r). (run-event-loc(run_local_pred(r;e)) = run-event-loc(e) ∈ Id)
6. ∀e:runEvents(r). (¬↓e run-lt(r) run_local_pred(r;e))
7. ∀e,x:runEvents(r).
     ((↓x run-lt(r) e)
     ⇒ (run-event-loc(x) = run-event-loc(e) ∈ Id)
     ⇒ ((↓run_local_pred(r;e) run-lt(r) e) ∧ (¬↓run_local_pred(r;e) run-lt(r) x)))
8. ∀x,y,z:runEvents(r).  ((↓x run-lt(r) y) ⇒ (↓y run-lt(r) z) ⇒ (↓x run-lt(r) z))
9. e1 : runEvents(r)@i
10. e2 : runEvents(r)@i
11. run-event-loc(e1) = run-event-loc(e2) ∈ Id
12. (↓e1 run-lt(r) e2) ⇒ (↑run-event-step(e1) <z run-event-step(e2))
13. (↓e1 run-lt(r) e2) ⇐ ↑run-event-step(e1) <z run-event-step(e2)
14. ¬↓e1 run-lt(r) e2@i
15. ¬↓e2 run-lt(r) e1@i
⊢ e1 = e2 ∈ runEvents(r)
BY
{ ((InstLemma `total-run-lt` [⌈M⌉;⌈r⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
   THEN RepeatFor 2 ((D -1 THEN Auto))
   THEN OnMaybeHyp 14 (\h. (D h THEN D 0 THEN Trivial))) }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)
4.  \mforall{}x,y:runEvents(r).    ((\mdownarrow{}x  run-lt(r)  y)  {}\mRightarrow{}  run-event-step(x)  <  run-event-step(y))
5.  \mforall{}e:runEvents(r).  (run-event-loc(run\_local\_pred(r;e))  =  run-event-loc(e))
6.  \mforall{}e:runEvents(r).  (\mneg{}\mdownarrow{}e  run-lt(r)  run\_local\_pred(r;e))
7.  \mforall{}e,x:runEvents(r).
          ((\mdownarrow{}x  run-lt(r)  e)
          {}\mRightarrow{}  (run-event-loc(x)  =  run-event-loc(e))
          {}\mRightarrow{}  ((\mdownarrow{}run\_local\_pred(r;e)  run-lt(r)  e)  \mwedge{}  (\mneg{}\mdownarrow{}run\_local\_pred(r;e)  run-lt(r)  x)))
8.  \mforall{}x,y,z:runEvents(r).    ((\mdownarrow{}x  run-lt(r)  y)  {}\mRightarrow{}  (\mdownarrow{}y  run-lt(r)  z)  {}\mRightarrow{}  (\mdownarrow{}x  run-lt(r)  z))
9.  e1  :  runEvents(r)@i
10.  e2  :  runEvents(r)@i
11.  run-event-loc(e1)  =  run-event-loc(e2)
12.  (\mdownarrow{}e1  run-lt(r)  e2)  {}\mRightarrow{}  (\muparrow{}run-event-step(e1)  <z  run-event-step(e2))
13.  (\mdownarrow{}e1  run-lt(r)  e2)  \mLeftarrow{}{}  \muparrow{}run-event-step(e1)  <z  run-event-step(e2)
14.  \mneg{}\mdownarrow{}e1  run-lt(r)  e2@i
15.  \mneg{}\mdownarrow{}e2  run-lt(r)  e1@i
\mvdash{}  e1  =  e2


By

---

Latex:
((InstLemma  `total-run-lt`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  ((D  -1  THEN  Auto))
  THEN  OnMaybeHyp  14  (\mbackslash{}h.  (D  h  THEN  D  0  THEN  Trivial)))

---

Home Index