---

Step * of Lemma nysiad_on_input_message_bag_wf

∀[M:ValueAllType]. ∀[add2baghdr,addwaitinghdr,adeliverhdr:Atom List]. ∀[deqM:EqDecider(M)].
∀[inputmsghdr,kdeliverhdr,readyhdr:Atom List]. ∀[senders:bag(Id)]. ∀[tooarcasthdr:Atom List].
∀[waitingmap:map-sig{i:l}(Id;M)].
∀[mf:nysiad_headers_type{i:l}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr)].
∀[msg2m:Message(mf) ─→ M].
  (nysiad_on_input_message_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;readyhdr;...;...;...;mf;...)
   ∈ Id
   ─→ (Message(mf) × Id? × Id + (Message(mf) × Id? × Id))
   ─→ ((M × Id? × Id) List × map-sig-map(waitingmap))
   ─→ bag(Interface))
BY
{ StartEmlProof }

1
1. M : {T:Type| valueall-type(T)} 
2. add2baghdr : Atom List
3. addwaitinghdr : Atom List
4. adeliverhdr : Atom List
5. deqM : EqDecider(M)
6. inputmsghdr : Atom List
7. kdeliverhdr : Atom List
8. readyhdr : Atom List
9. senders : bag(Id)
10. tooarcasthdr : Atom List
11. waitingmap : map-sig{i:l}(Id;M)
12. mf : nysiad_headers_type{i:l}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr)
13. (mf kdeliverhdr) = (Message(mf) × Id? × Id) ∈ Type
14. (mf tooarcasthdr) = (Message(mf) × Id? × Id) ∈ Type
15. (mf inputmsghdr) = (Message(mf) × Id? × Id) ∈ Type
16. (mf adeliverhdr) = (Id × Message(mf)) ∈ Type
17. (mf addwaitinghdr) = (Message(mf) × Id? × Id) ∈ Type
18. (mf add2baghdr) = (Message(mf) × Id? × Id) ∈ Type
19. (mf readyhdr) = Id ∈ Type
20. mf ∈ Name ─→ Type
21. msg2m : Message(mf) ─→ M
⊢ nysiad_on_input_message_bag(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;...;readyhdr;...;...;...;mf;msg2m)
  ∈ Id
  ─→ (Message(mf) × Id? × Id + (Message(mf) × Id? × Id))
  ─→ ((M × Id? × Id) List × map-sig-map(waitingmap))
  ─→ bag(Interface)

---

Latex:

---

Latex:
\mforall{}[M:ValueAllType].  \mforall{}[add2baghdr,addwaitinghdr,adeliverhdr:Atom  List].  \mforall{}[deqM:EqDecider(M)].
\mforall{}[inputmsghdr,kdeliverhdr,readyhdr:Atom  List].  \mforall{}[senders:bag(Id)].  \mforall{}[tooarcasthdr:Atom  List].
\mforall{}[waitingmap:map-sig\{i:l\}(Id;M)].
\mforall{}[...


By

---

Latex:
StartEmlProof

---

Home Index