---

Step * 1 2 2 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
⊢ 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
{ (Assert λc.fst(c) = x ∈ component(P.M[P]) ─→ 𝔹 BY
         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]) ─→ 𝔹
⊢ 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)

---

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
\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:
(Assert  \mlambda{}c.fst(c)  =  x  \mmember{}  component(P.M[P])  {}\mrightarrow{}  \mBbbB{}  BY
              Auto)

---

Home Index