---

Step * 1 1 3 2 1 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. 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)
⊢ ∃e:{tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
   (fst(e) < m
   ∧ (n ≤ (fst(e)))
   ∧ ((x = (snd(e)) ∈ Id) ∧ ((inl last(L1 @ L2)) = (inl e) ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?)))
   ∧ ((L2 @ [<m, x>])
     = (map(λt.<t, x>;filter(λt.is-run-event(r;t;x);[n, (fst(e)) + 1))) @ [<m, x>])
     ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)))
BY
{ (With ⌈last(L2)⌉ (D 0)⋅
   THEN Try (Complete ((Auto THEN RW assert_pushdownC 0 THEN Auto)))
   THEN (GenConcl ⌈last(L2) = X ∈ {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} ⌉⋅
         THENA (Auto THEN RW assert_pushdownC 0 THEN Auto)
         )
   THEN (Fold `mapfilter` 0 THEN Auto)⋅)⋅ }

1
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))
⊢ x = (snd(X)) ∈ Id

2
.....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. 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
⊢ last(L1 @ L2) = X ∈ {tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 

3
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 @ [<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)

4
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. e : {tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
18. X : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
19. last(L2) = X ∈ {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} @i
20. fst(e) < m
21. n ≤ (fst(e))
22. x = (snd(e)) ∈ Id
⊢ ¬↑null(L1 @ L2)

---

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.  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)
\mvdash{}  \mexists{}e:\{tx:\mBbbN{}  \mtimes{}  Id|  \muparrow{}is-run-event(r;fst(tx);snd(tx))\} 
      (fst(e)  <  m
      \mwedge{}  (n  \mleq{}  (fst(e)))
      \mwedge{}  ((x  =  (snd(e)))  \mwedge{}  ((inl  last(L1  @  L2))  =  (inl  e)))
      \mwedge{}  ((L2  @  [<m,  x>])  =  (map(\mlambda{}t.<t,  x>filter(\mlambda{}t.is-run-event(r;t;x);[n,  (fst(e))  +  1)))  @  [<m,  x>])\000C))


By

---

Latex:
(With  \mkleeneopen{}last(L2)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Try  (Complete  ((Auto  THEN  RW  assert\_pushdownC  0  THEN  Auto)))
  THEN  (GenConcl  \mkleeneopen{}last(L2)  =  X\mkleeneclose{}\mcdot{}  THENA  (Auto  THEN  RW  assert\_pushdownC  0  THEN  Auto))
  THEN  (Fold  `mapfilter`  0  THEN  Auto)\mcdot{})\mcdot{}

---

Home Index