---

Step * of Lemma run_local_pred_time

∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀e:runEvents(r).  ((fst(run_local_pred(r;e))) ≤ (fst(e)))
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
⊢ (fst(run-local-pred(r;e2;e1;e1))) ≤ e1

---

Latex:

---

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


By

---

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

---

Home Index