---

Step * 4 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 : runEvents(r)@i
8. x : runEvents(r)@i
9. x run-lt(r) e@i
10. run-event-loc(x) = run-event-loc(e) ∈ Id@i
⊢ ↓run_local_pred(r;e) run-lt(r) e
BY
{ (D 0
   THEN RepUR ``run-lt`` 0
   THEN BLemma `rel-rel-plus`
   THEN Auto
   THEN RepUR ``run-pred`` 0
   THEN OrLeft
   THEN Auto
   THEN (FLemma `run-lt-step-less` [-3] THENA Auto)) }

1
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 : runEvents(r)@i
8. x : runEvents(r)@i
9. x run-lt(r) e@i
10. run-event-loc(x) = run-event-loc(e) ∈ Id@i
11. run-event-loc(run_local_pred(r;e)) = run-event-loc(e) ∈ Id
12. run-event-step(x) < run-event-step(e)
⊢ run-event-step(run_local_pred(r;e)) < run-event-step(e)

---

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.  e  :  runEvents(r)@i
8.  x  :  runEvents(r)@i
9.  x  run-lt(r)  e@i
10.  run-event-loc(x)  =  run-event-loc(e)@i
\mvdash{}  \mdownarrow{}run\_local\_pred(r;e)  run-lt(r)  e


By

---

Latex:
(D  0
  THEN  RepUR  ``run-lt``  0
  THEN  BLemma  `rel-rel-plus`
  THEN  Auto
  THEN  RepUR  ``run-pred``  0
  THEN  OrLeft
  THEN  Auto
  THEN  (FLemma  `run-lt-step-less`  [-3]  THENA  Auto))

---

Home Index