---

Step * 2 of Lemma sequential-composition-inputs_wf


1. Info : Type
2. f : Name ─→ Type
3. X : EClass(Interface)
4. es : EO+(Info)
5. e : E
6. hdr : Name
7. single-valued-on-header{i:l}(Info;X;hdr)
8. ∀x:bag(Interface). (↑((λxs.(#([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)]) =z 1)) x) ∈ Type)
9. xs : bag(Interface)@i
10. ↑((λxs.(#([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)]) =z 1)) xs)@i
11. single-valued-bag([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)];Interface)
⊢ 0 < #([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)])
BY
{ (AllReduce THEN RW assert_pushdownC (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  f  :  Name  {}\mrightarrow{}  Type
3.  X  :  EClass(Interface)
4.  es  :  EO+(Info)
5.  e  :  E
6.  hdr  :  Name
7.  single-valued-on-header\{i:l\}(Info;X;hdr)
8.  \mforall{}x:bag(Interface)
          (\muparrow{}((\mlambda{}xs.(\#([x\mmember{}xs|name\_eq(msg-header(x.msg);hdr)  \mwedge{}\msubb{}  x.dst  =  loc(e)])  =\msubz{}  1))  x)  \mmember{}  Type)
9.  xs  :  bag(Interface)@i
10.  \muparrow{}((\mlambda{}xs.(\#([x\mmember{}xs|name\_eq(msg-header(x.msg);hdr)  \mwedge{}\msubb{}  x.dst  =  loc(e)])  =\msubz{}  1))  xs)@i
11.  single-valued-bag([x\mmember{}xs|name\_eq(msg-header(x.msg);hdr)  \mwedge{}\msubb{}  x.dst  =  loc(e)];Interface)
\mvdash{}  0  <  \#([x\mmember{}xs|name\_eq(msg-header(x.msg);hdr)  \mwedge{}\msubb{}  x.dst  =  loc(e)])


By

---

Latex:
(AllReduce  THEN  RW  assert\_pushdownC  (-2)  THEN  Auto)

---

Home Index