---

Step * of Lemma msg-interface-extensionality

∀[f:Name ─→ Type]. ∀[x,y:Interface].
  uiff(x = y ∈ Interface;(x.delay = y.delay ∈ ℤ) ∧ (x.dst = y.dst ∈ Id) ∧ (x.msg = y.msg ∈ Message(f)))
BY
{ (Auto
   THEN RepeatFor 2 (D -5)
   THEN RepeatFor 2 (D -4)
   THEN All
   (RepUR ``msg-interface-delay msg-interface-destination msg-interface-message``)⋅
   THEN Unfold `msg-interface` 0
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[x,y:Interface].
    uiff(x  =  y;(x.delay  =  y.delay)  \mwedge{}  (x.dst  =  y.dst)  \mwedge{}  (x.msg  =  y.msg))


By

---

Latex:
(Auto
  THEN  RepeatFor  2  (D  -5)
  THEN  RepeatFor  2  (D  -4)
  THEN  All
  (RepUR  ``msg-interface-delay  msg-interface-destination  msg-interface-message``)\mcdot{}
  THEN  Unfold  `msg-interface`  0
  THEN  EqCD
  THEN  Auto)

---

Home Index