Step
*
1
2
2
1
1
1
1
1
2
of Lemma
adjacent-run-states
1. [M] : Type ─→ Type
2. x : Id@i
3. v11 : Id@i
4. k : ℕ@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. ¬↑x = v11@i
8. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
9. u : component(P.M[P])@i
10. v : component(P.M[P]) List@i
11. ∀G:LabeledDAG(pInTransit(P.M[P])). ∀L:component(P.M[P]) List. ∀Z:Process(P.M[P]) List.
(Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⇒ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<L, G>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))@i
⊢ ∀G:LabeledDAG(pInTransit(P.M[P])). ∀L:component(P.M[P]) List. ∀Z:Process(P.M[P]) List.
(Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⇒ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;[u / v]) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
deliver-msg-to-comp(k;ms;v11;<L, G>;u))
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))
BY
{ (DVar `u'
THEN RepUR ``deliver-msg-to-comp mapfilter`` 0
THEN Folds ``mapfilter deliver-msg-to-comp`` 0
THEN RepeatFor 2 (AutoSplit)
THEN Auto) }
1
1. [M] : Type ─→ Type
2. x : Id@i
3. v11 : Id@i
4. k : ℕ@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. ¬↑x = v11@i
8. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
9. u1 : Id@i
10. ¬(u1 = v11 ∈ Id)
11. u2 : Process(P.M[P])@i
12. v : component(P.M[P]) List@i
13. ∀G:LabeledDAG(pInTransit(P.M[P])). ∀L:component(P.M[P]) List. ∀Z:Process(P.M[P]) List.
(Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⇒ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<L, G>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))@i
14. u1 = x ∈ Id
15. G : LabeledDAG(pInTransit(P.M[P]))@i
16. L : component(P.M[P]) List@i
17. Z : Process(P.M[P]) List@i
18. Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)@i
⊢ Z @ [u2 / map(λc.(snd(c));filter(λc.fst(c) = x;v))] ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<[<u1, u2> / L], G>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
2
1. [M] : Type ─→ Type
2. x : Id@i
3. v11 : Id@i
4. k : ℕ@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. ¬↑x = v11@i
8. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
9. u1 : Id@i
10. ¬(u1 = x ∈ Id)
11. u2 : Process(P.M[P])@i
12. v : component(P.M[P]) List@i
13. ∀G:LabeledDAG(pInTransit(P.M[P])). ∀L:component(P.M[P]) List. ∀Z:Process(P.M[P]) List.
(Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⇒ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<L, G>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))@i
14. u1 = v11 ∈ Id
15. G : LabeledDAG(pInTransit(P.M[P]))@i
16. L : component(P.M[P]) List@i
17. Z : Process(P.M[P]) List@i
18. Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)@i
⊢ Z @ map(λc.(snd(c));filter(λc.fst(c) = x;v)) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
let Q,ext = Process-apply(u2;ms)
in <[<u1, Q> / L], lg-append(G;add-cause(<k, v11>;ext))>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
3
1. [M] : Type ─→ Type
2. x : Id@i
3. v11 : Id@i
4. k : ℕ@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. ¬↑x = v11@i
8. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
9. u1 : Id@i
10. ¬(u1 = v11 ∈ Id)
11. ¬(u1 = x ∈ Id)
12. u2 : Process(P.M[P])@i
13. v : component(P.M[P]) List@i
14. ∀G:LabeledDAG(pInTransit(P.M[P])). ∀L:component(P.M[P]) List. ∀Z:Process(P.M[P]) List.
(Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⇒ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<L, G>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs))@i
15. G : LabeledDAG(pInTransit(P.M[P]))@i
16. L : component(P.M[P]) List@i
17. Z : Process(P.M[P]) List@i
18. Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)@i
⊢ Z @ map(λc.(snd(c));filter(λc.fst(c) = x;v)) ⊆ let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<[<u1, u2> / L], G>)
in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
Latex:
Latex:
1. [M] : Type {}\mrightarrow{} Type
2. x : Id@i
3. v11 : Id@i
4. k : \mBbbN{}@i
5. ms : pMsg(P.M[P])@i
6. Continuous+(P.M[P])@i'
7. \mneg{}\muparrow{}x = v11@i
8. \mlambda{}c.fst(c) = x \mmember{} component(P.M[P]) {}\mrightarrow{} \mBbbB{}
9. u : component(P.M[P])@i
10. v : component(P.M[P]) List@i
11. \mforall{}G:LabeledDAG(pInTransit(P.M[P])). \mforall{}L:component(P.M[P]) List. \mforall{}Z:Process(P.M[P]) List.
(Z \msubseteq{} mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;L)
{}\mRightarrow{} Z @ mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;v)
\msubseteq{} let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
<L, G>)
in mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs))@i
\mvdash{} \mforall{}G:LabeledDAG(pInTransit(P.M[P])). \mforall{}L:component(P.M[P]) List. \mforall{}Z:Process(P.M[P]) List.
(Z \msubseteq{} mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;L)
{}\mRightarrow{} Z @ mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;[u / v])
\msubseteq{} let Cs,G = accumulate (with value S and list item C):
deliver-msg-to-comp(k;ms;v11;S;C)
over list:
v
with starting value:
deliver-msg-to-comp(k;ms;v11;<L, G>u))
in mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;Cs))
By
Latex:
(DVar `u'
THEN RepUR ``deliver-msg-to-comp mapfilter`` 0
THEN Folds ``mapfilter deliver-msg-to-comp`` 0
THEN RepeatFor 2 (AutoSplit)
THEN Auto)
Home
Index