---

Step * 1 1 2 1 1 2 1 1 2 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. 0 < m
7. (n ≤ (m - 1))
⇒ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m - 1))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m - 1))
   = 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, m - 1))))) + 1))
   ∈ ((ℕ × Id) List))
8. n ≤ m@i
⊢ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))
   = 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, m))))) + 1))
   ∈ ((ℕ × Id) List))
BY
{ (Decide n ≤ (m - 1) THENA Auto) }

1
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. n : ℕ@i
4. x : Id@i
5. m : ℤ
6. 0 < m
7. (n ≤ (m - 1))
⇒ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m - 1))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m - 1))
   = 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, m - 1))))) + 1))
   ∈ ((ℕ × Id) List))
8. n ≤ m@i
9. n ≤ (m - 1)
⊢ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))
   = 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, m))))) + 1))
   ∈ ((ℕ × Id) List))

2
1. M : Type ─→ Type@i'
2. r : pRunType(P.M[P])@i
3. n : ℕ@i
4. x : Id@i
5. m : ℤ
6. 0 < m
7. (n ≤ (m - 1))
⇒ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m - 1))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m - 1))
   = 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, m - 1))))) + 1))
   ∈ ((ℕ × Id) List))
8. n ≤ m@i
9. ¬(n ≤ (m - 1))
⊢ (¬↑null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))))
⇒ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))
   = 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, m))))) + 1))
   ∈ ((ℕ × Id) List))

---

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.  0  <  m
7.  (n  \mleq{}  (m  -  1))
{}\mRightarrow{}  (\mneg{}\muparrow{}null(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m  -  1))))
{}\mRightarrow{}  (mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m  -  1))
      =  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,  m  -  1)))))  +  1)))
8.  n  \mleq{}  m@i
\mvdash{}  (\mneg{}\muparrow{}null(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m))))
{}\mRightarrow{}  (mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m))
      =  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,  m)))))  +  1)))


By

---

Latex:
(Decide  n  \mleq{}  (m  -  1)  THENA  Auto)

---

Home Index