---

Step * of Lemma make-Msg-equal

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

1
1. f : Name ─→ Type
2. hdr1 : Name
3. hdr2 : Name
4. val1 : f hdr1
5. val2 : f hdr2
6. ff = ff
7. <hdr1, val1> = <hdr2, val2> ∈ (h:Name × (f h))
⊢ val1 = val2 ∈ (f hdr1)

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdr1,hdr2:Name].  \mforall{}[val1:f  hdr1].  \mforall{}[val2:f  hdr2].
    (make-Msg(hdr1;val1)  =  make-Msg(hdr2;val2)  \mLeftarrow{}{}\mRightarrow{}  \{(hdr1  =  hdr2)  \mwedge{}  (val1  =  val2)\})


By

---

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

---

Home Index