---

Step * 1 2 2 1 1 1 1 1 1 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]) ─→ 𝔹
⊢ ∀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;L))
BY
{ (RepUR ``mapfilter`` 0 THEN Fold `mapfilter` 0 THEN Auto THEN RWO "append-nil" 0 THEN Auto)⋅ }

---

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{}
\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  @  []  \msubseteq{}  mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c)  =  x;L))


By

---

Latex:
(RepUR  ``mapfilter``  0  THEN  Fold  `mapfilter`  0  THEN  Auto  THEN  RWO  "append-nil"  0  THEN  Auto)\mcdot{}

---

Home Index