---

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


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. mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n))
= []
∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)@i
11. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List@i
12. ¬(L2 = [] ∈ ({tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List))
13. 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
14. [] = [] ∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)
15. ↑is-run-event(r;m;x)
16. X : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
17. last(L2) = X ∈ {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
18. fst(X) < m
19. n ≤ (fst(X))
20. x = (snd(X)) ∈ Id
21. X = X ∈ {tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
⊢ (L2 @ [<m, x>])
= (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, (fst(X)) + 1)) @ [<m, x>])
∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)
BY
{ (EqCD THEN Auto) }

1
.....subterm..... T:t
1:n
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. mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n))
= []
∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)@i
11. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List@i
12. ¬(L2 = [] ∈ ({tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List))
13. 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
14. [] = [] ∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)
15. ↑is-run-event(r;m;x)
16. X : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
17. last(L2) = X ∈ {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
18. fst(X) < m
19. n ≤ (fst(X))
20. x = (snd(X)) ∈ Id
21. X = 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))
∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)

---

Latex:

---

Latex:

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.  mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  n))  =  []@i
11.  L2  :  \{tx:\{n..m\msupminus{}\}  \mtimes{}  \{i:Id|  i  =  x\}  |  \muparrow{}is-run-event(r;fst(tx);snd(tx))\}    List@i
12.  \mneg{}(L2  =  [])
13.  mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m))  =  L2@i
14.  []  =  []
15.  \muparrow{}is-run-event(r;m;x)
16.  X  :  \{tx:\{n..m\msupminus{}\}  \mtimes{}  \{i:Id|  i  =  x\}  |  \muparrow{}is-run-event(r;fst(tx);snd(tx))\}  @i
17.  last(L2)  =  X@i
18.  fst(X)  <  m
19.  n  \mleq{}  (fst(X))
20.  x  =  (snd(X))
21.  X  =  X
\mvdash{}  (L2  @  [<m,  x>])  =  (mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  (fst(X))  +  1))  @  [<m,  x>])


By

---

Latex:
(EqCD  THEN  Auto)

---

Home Index