---

Step * of Lemma mk-msg-equal

∀[f:Name ⟶ Type]. ∀[auth1,auth2:𝔹]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
  (mk-msg(auth1;hdr1;val1) = mk-msg(auth2;hdr2;val2) ∈ Message(f)
  ⇐⇒ {auth1 = auth2 ∧ (hdr1 = hdr2 ∈ Name) ∧ (val1 = val2 ∈ (f hdr1))})
BY
{ (Unfold `guard` 0
   THEN Auto
   THEN RepUR ``mk-msg make-basicMsg Message basicMessage`` -1
   THEN EqHD (-1)
   THEN Auto
   THEN AllReduce) }

1
1. f : Name ⟶ Type
2. auth1 : 𝔹
3. auth2 : 𝔹
4. hdr1 : Name
5. hdr2 : Name
6. val1 : f hdr1
7. val2 : f hdr2
8. auth1 = auth2
9. <hdr1, val1> = <hdr2, val2> ∈ (h:Name × (f h))
⊢ val1 = val2 ∈ (f hdr1)

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[auth1,auth2:\mBbbB{}].  \mforall{}[hdr1,hdr2:Name].  \mforall{}[val1:f  hdr1].  \mforall{}[val2:f  hdr2].
    (mk-msg(auth1;hdr1;val1)  =  mk-msg(auth2;hdr2;val2)
    \mLeftarrow{}{}\mRightarrow{}  \{auth1  =  auth2  \mwedge{}  (hdr1  =  hdr2)  \mwedge{}  (val1  =  val2)\})


By

---

Latex:
(Unfold  `guard`  0
  THEN  Auto
  THEN  RepUR  ``mk-msg  make-basicMsg  Message  basicMessage``  -1
  THEN  EqHD  (-1)
  THEN  Auto
  THEN  AllReduce)

---

Home Index