---

Step * 1 1 of Lemma nysiad_on_input_message_bag_wf


1. M : Type
2. valueall-type(M)
3. add2baghdr : Atom List
4. addwaitinghdr : Atom List
5. adeliverhdr : Atom List
6. deqM : EqDecider(M)
7. inputmsghdr : Atom List
8. kdeliverhdr : Atom List
9. readyhdr : Atom List
10. senders : bag(Id)
11. tooarcasthdr : Atom List
12. waitingmap : map-sig{i:l}(Id;M)
13. mf : nysiad_headers_type{i:l}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr)
14. (mf kdeliverhdr) = (Message(mf) × Id? × Id) ∈ Type
15. (mf tooarcasthdr) = (Message(mf) × Id? × Id) ∈ Type
16. (mf inputmsghdr) = (Message(mf) × Id? × Id) ∈ Type
17. (mf adeliverhdr) = (Id × Message(mf)) ∈ Type
18. (mf addwaitinghdr) = (Message(mf) × Id? × Id) ∈ Type
19. (mf add2baghdr) = (Message(mf) × Id? × Id) ∈ Type
20. (mf readyhdr) = Id ∈ Type
21. mf ∈ Name ─→ Type
22. msg2m : Message(mf) ─→ M
23. slf : Id@i
24. i : Message(mf) × Id? × Id + (Message(mf) × Id? × Id)@i
25. s : (M × Id? × Id) List × map-sig-map(waitingmap)@i
26. isl(i) ∈ 𝔹
27. ↑isl(i)
⊢ nysiad_on_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;inputmsghdr;kdeliverhdr;readyhdr;...;...;mf;msg2m) 
  slf 
  outl(i) 
  s ∈ bag(Interface)
BY
{ (GenConclAtAddr [2;1;1;1] THEN Auto) }

---

Latex:

---

Latex:

1.  M  :  Type
2.  valueall-type(M)
3.  add2baghdr  :  Atom  List
4.  addwaitinghdr  :  Atom  List
5.  adeliverhdr  :  Atom  List
6.  deqM  :  EqDecider(M)
7.  inputmsghdr  :  Atom  List
8.  kdeliverhdr  :  Atom  List
9.  readyhdr  :  Atom  List
10.  senders  :  bag(Id)
11.  tooarcasthdr  :  Atom  List
12.  waitingmap  :  map-sig\{i:l\}(Id;M)
13.  mf  :  nysiad\_headers\_type\{i:l\}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;readyhdr;...)
14.  (mf  kdeliverhdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
15.  (mf  tooarcasthdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
16.  (mf  inputmsghdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
17.  (mf  adeliverhdr)  =  (Id  \mtimes{}  Message(mf))
18.  (mf  addwaitinghdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
19.  (mf  add2baghdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
20.  (mf  readyhdr)  =  Id
21.  mf  \mmember{}  Name  {}\mrightarrow{}  Type
22.  msg2m  :  Message(mf)  {}\mrightarrow{}  M
23.  slf  :  Id@i
24.  i  :  Message(mf)  \mtimes{}  Id?  \mtimes{}  Id  +  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)@i
25.  s  :  (M  \mtimes{}  Id?  \mtimes{}  Id)  List  \mtimes{}  map-sig-map(waitingmap)@i
26.  isl(i)  \mmember{}  \mBbbB{}
27.  \muparrow{}isl(i)
\mvdash{}  nysiad\_on\_addwaiting(M;add2baghdr;addwaitinghdr;adeliverhdr;deqM;...;...;readyhdr;...;...;mf;...) 
    slf 
    outl(i) 
    s  \mmember{}  bag(Interface)


By

---

Latex:
(GenConclAtAddr  [2;1;1;1]  THEN  Auto)

---

Home Index