---

Step * of Lemma nysiad_QueueState-classrel

∀[add2baghdr,addwaitinghdr,adeliverhdr,inputmsghdr,kdeliverhdr,readyhdr,tooarcasthdr:Atom List].
∀[mf:nysiad_headers_type{i:l}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr)].
  ∀es:EO+(Message(mf)). ∀e:E. ∀x:Id. ∀v:(Message(mf) × Id? × Id) List × 𝔹.
    (v ∈ nysiad_QueueState(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf) x(e)
    ⇐⇒ v
        = nysiad_QueueStateFun(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...;mf;x;es;e)
        ∈ ((Message(mf) × Id? × Id) List × 𝔹))
BY
{ ProveEmlLemma }

---

Latex:

---

Latex:
\mforall{}[add2baghdr,addwaitinghdr,adeliverhdr,inputmsghdr,kdeliverhdr,readyhdr,tooarcasthdr:Atom  List].
\mforall{}[...


By

---

Latex:
ProveEmlLemma

---

Home Index