---

Step * of Lemma run_local_pred_maximal

∀M:Type ─→ Type. ∀r:pRunType(P.M[P]). ∀e,x:runEvents(r).
  (run-event-step(x) < run-event-step(e)
  ⇒ run-event-step(run_local_pred(r;e)) < run-event-step(x)
  ⇒ (¬(run-event-loc(x) = run-event-loc(e) ∈ Id)))
BY
{ (Auto THEN D -4 THEN D -5 THEN D -3 THEN D -4 THEN All (RepUR ``run-event-step run_local_pred``) THEN All Reduce⋅) }

1
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. x1 : ℕ@i
7. x2 : Id@i
8. ↑is-run-event(r;x1;x2)@i
9. x1 < e1@i
10. fst(run-local-pred(r;e2;e1;e1)) < x1@i
⊢ ¬(run-event-loc(<x1, x2>) = run-event-loc(<e1, e2>) ∈ Id)

2
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. x1 : ℕ@i
7. x2 : Id@i
8. ↑is-run-event(r;x1;x2)@i
9. x1 < e1@i
10. fst(run-local-pred(r;e2;e1;e1)) < x1@i
⊢ run-event-loc(<x1, x2>) = run-event-loc(<e1, e2>) ∈ Id ∈ ℙ

3
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
6. x1 : ℕ@i
7. x2 : Id@i
8. ↑is-run-event(r;x1;x2)@i
9. x1 < e1@i
10. fst(run-local-pred(r;e2;e1;e1)) < x1@i
⊢ run-event-loc(<x1, x2>) = run-event-loc(<e1, e2>) ∈ Id ∈ ℙ

---

Latex:

---

Latex:
\mforall{}M:Type  {}\mrightarrow{}  Type.  \mforall{}r:pRunType(P.M[P]).  \mforall{}e,x:runEvents(r).
    (run-event-step(x)  <  run-event-step(e)
    {}\mRightarrow{}  run-event-step(run\_local\_pred(r;e))  <  run-event-step(x)
    {}\mRightarrow{}  (\mneg{}(run-event-loc(x)  =  run-event-loc(e))))


By

---

Latex:
(Auto
  THEN  D  -4
  THEN  D  -5
  THEN  D  -3
  THEN  D  -4
  THEN  All  (RepUR  ``run-event-step  run\_local\_pred``)
  THEN  All  Reduce\mcdot{})

---

Home Index