---

Step * 1 of Lemma prior-run-events_wf


1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. t : ℕ
4. ∀x:ℕ. (↑((λt.isl(fst((r t)))) x) ∈ Type)
5. t1 : ℕ@i
6. ↑((λt.isl(fst((r t)))) t1)@i
⊢ <t1, fst(snd(outl(fst((r t1)))))> ∈ runEvents(r)
BY
{ (MemTypeCD THEN Reduce 0 THEN Auto) }

1
1. M : Type ─→ Type
2. r : pRunType(P.M[P])
3. t : ℕ
4. ∀x:ℕ. (↑((λt.isl(fst((r t)))) x) ∈ Type)
5. t1 : ℕ@i
6. ↑((λt.isl(fst((r t)))) t1)@i
⊢ ↑is-run-event(r;t1;fst(snd(outl(fst((r t1))))))

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type
2.  r  :  pRunType(P.M[P])
3.  t  :  \mBbbN{}
4.  \mforall{}x:\mBbbN{}.  (\muparrow{}((\mlambda{}t.isl(fst((r  t))))  x)  \mmember{}  Type)
5.  t1  :  \mBbbN{}@i
6.  \muparrow{}((\mlambda{}t.isl(fst((r  t))))  t1)@i
\mvdash{}  <t1,  fst(snd(outl(fst((r  t1)))))>  \mmember{}  runEvents(r)


By

---

Latex:
(MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index