---

Step * of Lemma run_local_pred_wf

∀[M:Type ⟶ Type]. ∀r:pRunType(P.M[P]). ∀e:runEvents(r).  (run_local_pred(r;e) ∈ runEvents(r))
BY
{ (Auto THEN D -1 THEN D -2 THEN Unfold `run_local_pred` 0 THEN All Reduce  THEN MemTypeCD THEN Auto) }

1
.....set predicate..... 
1. M : Type ⟶ Type
2. r : pRunType(P.M[P])@i
3. e1 : ℕ@i
4. e2 : Id@i
5. ↑is-run-event(r;e1;e2)@i
⊢ ↑is-run-event(r;fst(run-local-pred(r;e2;e1;e1));snd(run-local-pred(r;e2;e1;e1)))

---

Latex:

---

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


By

---

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

---

Home Index