---

Step * 1 2 2 1 1 1 of Lemma adjacent-run-states


1. [M] : Type ─→ Type
2. x : Id@i
3. v3 : component(P.M[P]) List@i
4. v11 : Id@i
5. k : ℕ@i
6. ms : pMsg(P.M[P])@i
7. G : LabeledDAG(pInTransit(P.M[P]))@i
8. Continuous+(P.M[P])@i'
9. ¬↑x = v11@i
10. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = deliver-msg(k;ms;v11;v3;G) 
                                            in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)
BY
{ ((Auto THEN RepUR ``deliver-msg`` 0)
   THEN (GenConcl ⌈[] = L ∈ (component(P.M[P]) List)⌉⋅ THENA Auto)
   THEN Subst' mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ~ [] @ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) 0
   THEN Try ((Reduce  0 THEN CompleteAuto))⋅
   THEN (GenConcl ⌈[] = Z ∈ (Process(P.M[P]) List)⌉⋅ THENA Auto)
   THEN (Assert Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L) BY
               ((BLemma `l_contains_weakening` THEN Auto) THEN SubstFor ⌈L⌉ 0⋅ THEN Reduce 0 THEN Auto))⋅)⋅ }

1
1. [M] : Type ─→ Type
2. x : Id@i
3. v3 : component(P.M[P]) List@i
4. v11 : Id@i
5. k : ℕ@i
6. ms : pMsg(P.M[P])@i
7. G : LabeledDAG(pInTransit(P.M[P]))@i
8. Continuous+(P.M[P])@i'
9. ¬↑x = v11@i
10. λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹
11. L : component(P.M[P]) List@i
12. [] = L ∈ (component(P.M[P]) List)@i
13. Z : Process(P.M[P]) List@i
14. [] = Z ∈ (Process(P.M[P]) List)@i
15. Z ⊆ mapfilter(λc.(snd(c));λc.fst(c) = x;L)
⊢ Z @ mapfilter(λc.(snd(c));λc.fst(c) = x;v3) ⊆ let Cs,G = accumulate (with value S and list item C):
                                                            deliver-msg-to-comp(k;ms;v11;S;C)
                                                           over list:
                                                             v3
                                                           with starting value:
                                                            <L, G>) 
                                                in mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)

---

Latex:

---

Latex:

1.  [M]  :  Type  {}\mrightarrow{}  Type
2.  x  :  Id@i
3.  v3  :  component(P.M[P])  List@i
4.  v11  :  Id@i
5.  k  :  \mBbbN{}@i
6.  ms  :  pMsg(P.M[P])@i
7.  G  :  LabeledDAG(pInTransit(P.M[P]))@i
8.  Continuous+(P.M[P])@i'
9.  \mneg{}\muparrow{}x  =  v11@i
10.  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;v3)  \msubseteq{}  let  Cs,G  =  deliver-msg(k;ms;v11;v3;G) 
                                                                                        in  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;Cs)


By

---

Latex:
((Auto  THEN  RepUR  ``deliver-msg``  0)
  THEN  (GenConcl  \mkleeneopen{}[]  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Subst'  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;v3)  \msim{}  []
  @  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;v3)  0
  THEN  Try  ((Reduce    0  THEN  CompleteAuto))\mcdot{}
  THEN  (GenConcl  \mkleeneopen{}[]  =  Z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Assert  Z  \msubseteq{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;L)  BY
                          ((BLemma  `l\_contains\_weakening`  THEN  Auto)
                            THEN  SubstFor  \mkleeneopen{}L\mkleeneclose{}  0\mcdot{}
                            THEN  Reduce  0
                            THEN  Auto))\mcdot{})\mcdot{}

---

Home Index