---

Step * of Lemma Message-extensionality

∀[f:Name ⟶ Type]. ∀[m1,m2:Message(f)].
  uiff(m1 = m2 ∈ Message(f);msg-authentic(m1) = msg-authentic(m2)
  ∧ (msg-header(m1) = msg-header(m2) ∈ Name)
  ∧ (msg-body(m1) = msg-body(m2) ∈ (f msg-header(m1))))
BY
{ (Auto
   THEN RepeatFor 2 (D -5)
   THEN RepeatFor 2 (D -4)
   THEN RepUR ``Message basicMessage`` 0
   THEN All(RepUR ``msg-header msg-body msg-msg msg-authentic``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[m1,m2:Message(f)].
    uiff(m1  =  m2;msg-authentic(m1)  =  msg-authentic(m2)
    \mwedge{}  (msg-header(m1)  =  msg-header(m2))
    \mwedge{}  (msg-body(m1)  =  msg-body(m2)))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -5)
  THEN  RepeatFor  2  (D  -4)
  THEN  RepUR  ``Message  basicMessage``  0
  THEN  All(RepUR  ``msg-header  msg-body  msg-msg  msg-authentic``)
  THEN  Auto)

---

Home Index