Step
*
1
1
3
2
2
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. u : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}
11. v : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List
12. ¬([u / v] = [] ∈ ({tx:ℕn × {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);[0, n))
= [u / v]
∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List)@i
14. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List@i
15. 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
16. ↑is-run-event(r;m;x)
17. ¬↑null(L2)
⊢ ((inl last([u / (v @ L2)])) = (inl last([u / v])) ∈ ({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)) ∈ ℙ
BY
{ MemCD }
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. u : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}
11. v : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List
12. ¬([u / v] = [] ∈ ({tx:ℕn × {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);[0, n))
= [u / v]
∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List)@i
14. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List@i
15. 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
16. ↑is-run-event(r;m;x)
17. ¬↑null(L2)
⊢ (inl last([u / (v @ L2)])) = (inl last([u / v])) ∈ ({tx:ℕ × Id| ↑is-run-event(r;fst(tx);snd(tx))} ?) ∈ ℙ
2
.....subterm..... T:t
2: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. u : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))}
11. v : {tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List
12. ¬([u / v] = [] ∈ ({tx:ℕn × {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);[0, n))
= [u / v]
∈ ({tx:ℕn × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List)@i
14. L2 : {tx:{n..m-} × {i:Id| i = x ∈ Id} | ↑is-run-event(r;fst(tx);snd(tx))} List@i
15. 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
16. ↑is-run-event(r;m;x)
17. ¬↑null(L2)
⊢ (L2 @ [<m, x>]) = [<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)
10. u : \{tx:\mBbbN{}n \mtimes{} \{i:Id| i = x\} | \muparrow{}is-run-event(r;fst(tx);snd(tx))\}
11. v : \{tx:\mBbbN{}n \mtimes{} \{i:Id| i = x\} | \muparrow{}is-run-event(r;fst(tx);snd(tx))\} List
12. \mneg{}([u / v] = [])
13. mapfilter(\mlambda{}t.<t, x>\mlambda{}t.is-run-event(r;t;x);[0, n)) = [u / v]@i
14. L2 : \{tx:\{n..m\msupminus{}\} \mtimes{} \{i:Id| i = x\} | \muparrow{}is-run-event(r;fst(tx);snd(tx))\} List@i
15. mapfilter(\mlambda{}t.<t, x>\mlambda{}t.is-run-event(r;t;x);[n, m)) = L2@i
16. \muparrow{}is-run-event(r;m;x)
17. \mneg{}\muparrow{}null(L2)
\mvdash{} ((inl last([u / (v @ L2)])) = (inl last([u / v]))) \mwedge{} ((L2 @ [<m, x>]) = [<m, x>]) \mmember{} \mBbbP{}
By
Latex:
MemCD
Home
Index