---

Step * of Lemma run_local_pred_loc

∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e:runEvents(r).  ((snd(run_local_pred(r;e))) = (snd(e)) ∈ Id)
BY
{ (Auto THEN D -1 THEN D -2 THEN Unfold `run_local_pred` 0 THEN All Reduce  THEN Thin (-1)) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
⊢ (snd(run-local-pred(r;e2;e1;e1))) = e2 ∈ Id

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}r:pRunType(P.M[P]).  \mforall{}e:runEvents(r).    ((snd(run\_local\_pred(r;e)))  =  (snd(e)))


By

---

Latex:
(Auto  THEN  D  -1  THEN  D  -2  THEN  Unfold  `run\_local\_pred`  0  THEN  All  Reduce    THEN  Thin  (-1))

---

Home Index