---

Step * 1 of Lemma nysiad_on_input_message_bag_wf


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)
BY
{ At ⌜Type⌝ (ProveWfLemmaAux EmlAuto)⋅ }

1
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)

---

Latex:

---

Latex:

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;...;readyhdr;...)
13.  (mf  kdeliverhdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
14.  (mf  tooarcasthdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
15.  (mf  inputmsghdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
16.  (mf  adeliverhdr)  =  (Id  \mtimes{}  Message(mf))
17.  (mf  addwaitinghdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
18.  (mf  add2baghdr)  =  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id)
19.  (mf  readyhdr)  =  Id
20.  mf  \mmember{}  Name  {}\mrightarrow{}  Type
21.  msg2m  :  Message(mf)  {}\mrightarrow{}  M
\mvdash{}  nysiad\_on\_input\_message\_bag(M;add2baghdr;addwaitinghdr;...;deqM;...;...;...;...;...;...;mf;msg2m)
    \mmember{}  Id
    {}\mrightarrow{}  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id  +  (Message(mf)  \mtimes{}  Id?  \mtimes{}  Id))
    {}\mrightarrow{}  ((M  \mtimes{}  Id?  \mtimes{}  Id)  List  \mtimes{}  map-sig-map(waitingmap))
    {}\mrightarrow{}  bag(Interface)


By

---

Latex:
At  \mkleeneopen{}Type\mkleeneclose{}  (ProveWfLemmaAux  EmlAuto)\mcdot{}

---

Home Index