---

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

.....assertion..... 
1. M : Type ─→ Type
2. S0 : System(P.M[P])@i
3. r : pRunType(P.M[P])@i
4. n : ℕ@i
5. x : Id@i
6. m : ℕ@i
7. n ≤ m
8. ↑is-run-event(r;m;x)
9. ↑is-run-event(r;n;x)
10. L1 : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List@i
11. ¬(L1 = [] ∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List))
12. mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n))
= L1
∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)@i
13. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List@i
14. mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m))
= L2
∈ ({tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)@i
15. ↑is-run-event(r;m;x)
16. ¬↑null(L2)
17. X : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
18. last(L2) = X ∈ {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
19. fst(X) < m
20. n ≤ (fst(X))
21. x = (snd(X)) ∈ Id
22. last(L1 @ L2) = X ∈ {tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
⊢ L2 = mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, (fst(X)) + 1)) ∈ ((ℕ × Id) List)
BY
{ ((Assert ¬↑null(L2) BY
          Trivial)
   THEN MoveToConcl (-1)
   THEN RevHypSubst' 18 0
   THEN RevHypSubst' 14 0
   THEN Lemmaize [7]
   THEN Auto
   THEN NatInd (-3)
   THEN (D 0 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. 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))

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
⊢ (¬↑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:
.....assertion..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  S0  :  System(P.M[P])@i
3.  r  :  pRunType(P.M[P])@i
4.  n  :  \mBbbN{}@i
5.  x  :  Id@i
6.  m  :  \mBbbN{}@i
7.  n  \mleq{}  m
8.  \muparrow{}is-run-event(r;m;x)
9.  \muparrow{}is-run-event(r;n;x)
10.  L1  :  \{tx:\mBbbN{}n  \mtimes{}  \{i:Id|  i  =  x\}  |  \muparrow{}is-run-event(r;fst(tx);snd(tx))\}    List@i
11.  \mneg{}(L1  =  [])
12.  mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  n))  =  L1@i
13.  L2  :  \{tx:\{n..m\msupminus{}\}  \mtimes{}  \{i:Id|  i  =  x\}  |  \muparrow{}is-run-event(r;fst(tx);snd(tx))\}    List@i
14.  mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m))  =  L2@i
15.  \muparrow{}is-run-event(r;m;x)
16.  \mneg{}\muparrow{}null(L2)
17.  X  :  \{tx:\{n..m\msupminus{}\}  \mtimes{}  \{i:Id|  i  =  x\}  |  \muparrow{}is-run-event(r;fst(tx);snd(tx))\}  @i
18.  last(L2)  =  X@i
19.  fst(X)  <  m
20.  n  \mleq{}  (fst(X))
21.  x  =  (snd(X))
22.  last(L1  @  L2)  =  X
\mvdash{}  L2  =  mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  (fst(X))  +  1))


By

---

Latex:
((Assert  \mneg{}\muparrow{}null(L2)  BY
                Trivial)
  THEN  MoveToConcl  (-1)
  THEN  RevHypSubst'  18  0
  THEN  RevHypSubst'  14  0
  THEN  Lemmaize  [7]
  THEN  Auto
  THEN  NatInd  (-3)
  THEN  (D  0  THENA  Auto))

---

Home Index