---

Step * of Lemma run-eo_wf

∀[M:Type ─→ Type]. ∀[r:pRunType(P.M[P])].
  EO(r) ∈ EO+(pMsg(P.M[P])) supposing ∀e:runEvents(r). fst(fst(run-info(r;e))) < run-event-step(e)
BY
{ (Auto THEN Unfold `run-eo` 0 THEN MemCD THEN Reduce 0 THEN 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 : runEvents(r)@i
5. y : runEvents(r)@i
6. x run-lt(r) y@i
⊢ run-event-step(x) < run-event-step(y)

2
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)@i
⊢ run-event-loc(run_local_pred(r;e)) = run-event-loc(e) ∈ Id

3
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)@i
⊢ ¬↓e run-lt(r) run_local_pred(r;e)

4
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

5
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_local_pred(r;e) run-lt(r) e
⊢ ¬↓run_local_pred(r;e) run-lt(r) x

6
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 : runEvents(r)@i
9. y : runEvents(r)@i
10. z : runEvents(r)@i
11. x run-lt(r) y@i
12. y run-lt(r) z@i
⊢ ↓x run-lt(r) z

7
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. ↑run-event-step(e1) <z run-event-step(e2)@i
⊢ ↓e1 run-lt(r) e2

8
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)

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].
    EO(r)  \mmember{}  EO+(pMsg(P.M[P]))  supposing  \mforall{}e:runEvents(r).  fst(fst(run-info(r;e)))  <  run-event-step(e)


By

---

Latex:
(Auto  THEN  Unfold  `run-eo`  0  THEN  MemCD  THEN  Reduce  0  THEN  Auto)

---

Home Index