---

Step * 1 1 2 1 1 2 1 1 1 of Lemma run-event-cases


1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. n : ℕ@i
4. x : Id@i
5. m : ℤ
6. n ≤ 0@i
⊢ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, 0))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, 0))
   = mapfilter(λt.<t, x>;
               λt.is-run-event(r;t;x);
               [n, (fst(last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, 0))))) + 1))
   ∈ ((ℕ × Id) List))
BY
{ (Subst ⌈n ~ 0⌉ 0⋅ THEN Try (Complete (Auto)) THEN Subst ⌈[0, 0) ~ []⌉ 0⋅ THEN (RepUR ``mapfilter`` 0 THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  M  :  Type  {}\mrightarrow{}  Type@i'
2.  r  :  pRunType(P.M[P])@i
3.  n  :  \mBbbN{}@i
4.  x  :  Id@i
5.  m  :  \mBbbZ{}
6.  n  \mleq{}  0@i
\mvdash{}  (\mneg{}\muparrow{}null(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  0))))
{}\mRightarrow{}  (mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  0))
      =  mapfilter(\mlambda{}t.<t,  x>
                              \mlambda{}t.is-run-event(r;t;x);
                              [n,  (fst(last(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  0)))))  +  1)))


By

---

Latex:
(Subst  \mkleeneopen{}n  \msim{}  0\mkleeneclose{}  0\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Subst  \mkleeneopen{}[0,  0)  \msim{}  []\mkleeneclose{}  0\mcdot{}
  THEN  (RepUR  ``mapfilter``  0  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index