---

Step * of Lemma member-prior-run-events

∀[M:Type ─→ Type]. ∀r:pRunType(P.M[P]). ∀t:ℕ. ∀e:runEvents(r).  ((e ∈ prior-run-events(r;t)) ⇐⇒ run-event-step(e) < t)
BY
{ (Auto THEN All (RepUR ``prior-run-events run-event-step``)) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. t : ℕ@i
4. e : runEvents(r)@i
5. (e ∈ mapfilter(λt.<t, fst(snd(outl(fst((r t)))))>;λt.isl(fst((r t)));upto(t)))@i
⊢ fst(e) < t

2
1. [M] : Type ─→ Type
2. r : pRunType(P.M[P])@i
3. t : ℕ@i
4. e : runEvents(r)@i
5. fst(e) < t@i
⊢ (e ∈ mapfilter(λt.<t, fst(snd(outl(fst((r t)))))>;λt.isl(fst((r t)));upto(t)))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}r:pRunType(P.M[P]).  \mforall{}t:\mBbbN{}.  \mforall{}e:runEvents(r).
        ((e  \mmember{}  prior-run-events(r;t))  \mLeftarrow{}{}\mRightarrow{}  run-event-step(e)  <  t)


By

---

Latex:
(Auto  THEN  All  (RepUR  ``prior-run-events  run-event-step``))

---

Home Index