---

Step * 1 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)
⊢ ((if null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
then inr ⋅ 
else inl last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
fi 
= if null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n)))
  then inr ⋅ 
  else inl last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, n)))
  fi 
∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?))
∧ (mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[n, m + 1))
  = [<m, x>]
  ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)))
∨ (∃e:{tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
    (fst(e) < m
    ∧ (n ≤ (fst(e)))
    ∧ ((x = (snd(e)) ∈ Id)
      ∧ (if null(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
        then inr ⋅ 
        else inl last(mapfilter(λt.<t, x>;λt.is-run-event(r;t;x);[0, m)))
        fi 
        = (inl e)
        ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?)))
    ∧ (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(e)) + 1)) @ [<m, x>])
      ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List))))
BY
{ (((InstLemma `from-upto-split` [⌈0⌉;⌈m⌉;⌈n⌉]⋅ THENA Auto) THEN HypSubst' (-1) 0 THEN Thin (-1))
   THEN (InstLemma `from-upto-split` [⌈n⌉;⌈m + 1⌉;⌈m⌉]⋅ THENA Auto)
   THEN HypSubst' (-1) 0
   THEN Thin (-1)
   THEN (RWW "mapfilter-append null_append" 0 THENA Auto)
   THEN (GenConcl ⌈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)⌉⋅
         THENA Auto
         )
   THEN (GenConcl ⌈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)⌉⋅
         THENA Auto
         )
   THEN Subst ⌈[m, m + 1) ~ [m]⌉ 0⋅
   THEN Try ((RecUnfold `from-upto` 0
              THEN AutoSplit
              THEN (CallByValueReduce 0 THENA Auto)
              THEN EqCD
              THEN Try (Trivial)
              THEN RecUnfold `from-upto` 0⋅
              THEN AutoSplit))
   THEN RepUR ``mapfilter`` 0
   THEN Repeat (AutoSplit)) }

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. 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
12. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List@i
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. L1 = [] ∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)
15. L2 = [] ∈ ({tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)
16. ↑is-run-event(r;m;x)
⊢ (((inr ⋅ ) = (inr ⋅ ) ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?))
∧ ((L2 @ [<m, x>]) = [<m, x>] ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)))
∨ (∃e:{tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} 
    (fst(e) < m
    ∧ (n ≤ (fst(e)))
    ∧ ((x = (snd(e)) ∈ Id) ∧ ((inr ⋅ ) = (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))))

2
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. 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
12. L2 : {tx:{n..m-} × {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))
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. L1 = [] ∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}  List)
16. ↑is-run-event(r;m;x)
⊢ (((inl last(L1 @ L2)) = (inr ⋅ ) ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?))
∧ ((L2 @ [<m, x>]) = [<m, x>] ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)))
∨ (∃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))))

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)
⊢ (((inl last(L1 @ L2)) = (inl last(L1)) ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?))
∧ ((L2 @ [<m, x>]) = [<m, x>] ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))}  List)))
∨ (∃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))))

---

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)
\mvdash{}  ((if  null(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  m)))
then  inr  \mcdot{} 
else  inl  last(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  m)))
fi 
=  if  null(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  n)))
    then  inr  \mcdot{} 
    else  inl  last(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  n)))
    fi  )
\mwedge{}  (mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m  +  1))  =  [<m,  x>]))
\mvee{}  (\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{}  (if  null(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  m)))
                then  inr  \mcdot{} 
                else  inl  last(mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  m)))
                fi 
                =  (inl  e)))
        \mwedge{}  (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(e))  +  1))  @  [<m,  x>]))))


By

---

Latex:
(((InstLemma  `from-upto-split`  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  HypSubst'  (-1)  0  THEN  Thin  (-1))
  THEN  (InstLemma  `from-upto-split`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}m  +  1\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  HypSubst'  (-1)  0
  THEN  Thin  (-1)
  THEN  (RWW  "mapfilter-append  null\_append"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[0,  n))  =  L1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}mapfilter(\mlambda{}t.<t,  x>\mlambda{}t.is-run-event(r;t;x);[n,  m))  =  L2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Subst  \mkleeneopen{}[m,  m  +  1)  \msim{}  [m]\mkleeneclose{}  0\mcdot{}
  THEN  Try  ((RecUnfold  `from-upto`  0
                        THEN  AutoSplit
                        THEN  (CallByValueReduce  0  THENA  Auto)
                        THEN  EqCD
                        THEN  Try  (Trivial)
                        THEN  RecUnfold  `from-upto`  0\mcdot{}
                        THEN  AutoSplit))
  THEN  RepUR  ``mapfilter``  0
  THEN  Repeat  (AutoSplit))

---

Home Index