---

Step * of Lemma sequential-composition-inputs_wf

∀[Info:Type]. ∀[f:Name ─→ Type]. ∀[X:EClass(Interface)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[hdr:Name].
  sequential-composition-inputs(es;e;X;hdr) ∈ Message(f) List supposing single-valued-on-header{i:l}(Info;X;hdr)
BY
{ ProveWfLemma }

1
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
⊢ single-valued-bag([x∈xs|name_eq(msg-header(x.msg);hdr) ∧b x.dst = loc(e)];Interface)

2
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)])

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[X:EClass(Interface)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[hdr:Name].
    sequential-composition-inputs(es;e;X;hdr)  \mmember{}  Message(f)  List 
    supposing  single-valued-on-header\{i:l\}(Info;X;hdr)


By

---

Latex:
ProveWfLemma

---

Home Index