---

Step * of Lemma interface-cmp-zero

∀[f:Name ─→ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)].
∀[x,y:Interface(to locs, with hdrs)].
  (((interface-cmp(mcmp;locs;hdrs) x y) = 0 ∈ ℤ)
  ⇒ {(x.delay = y.delay ∈ ℤ)
     ∧ (x.dst = y.dst ∈ Id)
     ∧ msg-authentic(x.msg) = msg-authentic(y.msg)
     ∧ (msg-header(x.msg) = msg-header(y.msg) ∈ Name)
     ∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ)})
BY
{ (Auto
   THEN (Assert list-index-cmp(IdDeq;locs;λmi.mi.dst) ∈ comparison(Interface(to locs, with hdrs)) BY
               ((InstLemma `list-index-cmp_wf` [⌈Id⌉;⌈IdDeq⌉;⌈locs⌉;⌈Interface(to locs, with hdrs)⌉;⌈λmi.mi.dst⌉]⋅
                 THENA Auto
                 )
                THEN DoSubsume
                THEN Try (Trivial)
                THEN (BLemma `subtype_rel_comparison` THENA Auto)
                THEN Reduce 0
                THEN (D 0 THENA Auto)
                THEN D -1
                THEN MemTypeCD
                THEN Auto))
   THEN (Assert list-index-cmp(NameDeq;hdrs;λmi.msg-header(mi.msg)) ∈ comparison(Interface(to locs, with hdrs)) BY
               ((InstLemma `list-index-cmp_wf` [⌈Name⌉;⌈NameDeq⌉;⌈hdrs⌉;⌈Interface(to locs, with hdrs)⌉;
                 ⌈λmi.msg-header(mi.msg)⌉]⋅
                 THENA Auto
                 )
                THEN DoSubsume
                THEN Try (Trivial)
                THEN (BLemma `subtype_rel_comparison` THENA Auto)
                THEN Reduce 0
                THEN (D 0 THENA Auto)
                THEN D -1
                THEN MemTypeCD
                THEN Auto))
   THEN (Assert compare-fun(message-cmp(hdrs;mcmp);λmi.mi.msg) ∈ comparison(Interface(to locs, with hdrs)) BY
               (Using [`B',⌈{m:Message(f)| (msg-header(m) ∈ hdrs)} ⌉] MemCD⋅ THEN Auto THEN D -1 THEN Auto))
   THEN RepeatFor 3 (PromoteHyp (-1) 5)) }

1
1. f : Name ─→ Type
2. locs : Id List
3. hdrs : Name List
4. mcmp : hdr:Name ─→ comparison(f hdr)
5. list-index-cmp(IdDeq;locs;λmi.mi.dst) ∈ comparison(Interface(to locs, with hdrs))
6. list-index-cmp(NameDeq;hdrs;λmi.msg-header(mi.msg)) ∈ comparison(Interface(to locs, with hdrs))
7. compare-fun(message-cmp(hdrs;mcmp);λmi.mi.msg) ∈ comparison(Interface(to locs, with hdrs))
8. x : Interface(to locs, with hdrs)
9. y : Interface(to locs, with hdrs)
10. (interface-cmp(mcmp;locs;hdrs) x y) = 0 ∈ ℤ@i
⊢ {(x.delay = y.delay ∈ ℤ)
∧ (x.dst = y.dst ∈ Id)
∧ msg-authentic(x.msg) = msg-authentic(y.msg)
∧ (msg-header(x.msg) = msg-header(y.msg) ∈ Name)
∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ)}

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[locs:Id  List].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].
\mforall{}[x,y:Interface(to  locs,  with  hdrs)].
    (((interface-cmp(mcmp;locs;hdrs)  x  y)  =  0)
    {}\mRightarrow{}  \{(x.delay  =  y.delay)
          \mwedge{}  (x.dst  =  y.dst)
          \mwedge{}  msg-authentic(x.msg)  =  msg-authentic(y.msg)
          \mwedge{}  (msg-header(x.msg)  =  msg-header(y.msg))
          \mwedge{}  ((mcmp  msg-header(x.msg)  msg-body(x.msg)  msg-body(y.msg))  =  0)\})


By

---

Latex:
(Auto
  THEN  (Assert  list-index-cmp(IdDeq;locs;\mlambda{}mi.mi.dst)  \mmember{}  comparison(Interface(to  locs,  with  hdrs))  BY
                          ((InstLemma  `list-index-cmp\_wf`  [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}IdDeq\mkleeneclose{};\mkleeneopen{}locs\mkleeneclose{};\mkleeneopen{}Interface(to  locs,  with  hdrs)\mkleeneclose{};
                              \mkleeneopen{}\mlambda{}mi.mi.dst\mkleeneclose{}]\mcdot{}
                              THENA  Auto
                              )
                            THEN  DoSubsume
                            THEN  Try  (Trivial)
                            THEN  (BLemma  `subtype\_rel\_comparison`  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto))
  THEN  (Assert  list-index-cmp(NameDeq;hdrs;\mlambda{}mi.msg-header(mi.msg))
                            \mmember{}  comparison(Interface(to  locs,  with  hdrs))  BY
                          ((InstLemma  `list-index-cmp\_wf`  [\mkleeneopen{}Name\mkleeneclose{};\mkleeneopen{}NameDeq\mkleeneclose{};\mkleeneopen{}hdrs\mkleeneclose{};
                              \mkleeneopen{}Interface(to  locs,  with  hdrs)\mkleeneclose{};\mkleeneopen{}\mlambda{}mi.msg-header(mi.msg)\mkleeneclose{}]\mcdot{}
                              THENA  Auto
                              )
                            THEN  DoSubsume
                            THEN  Try  (Trivial)
                            THEN  (BLemma  `subtype\_rel\_comparison`  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (D  0  THENA  Auto)
                            THEN  D  -1
                            THEN  MemTypeCD
                            THEN  Auto))
  THEN  (Assert  compare-fun(message-cmp(hdrs;mcmp);\mlambda{}mi.mi.msg)
                            \mmember{}  comparison(Interface(to  locs,  with  hdrs))  BY
                          (Using  [`B',\mkleeneopen{}\{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\}  \mkleeneclose{}]  MemCD\mcdot{}
                            THEN  Auto
                            THEN  D  -1
                            THEN  Auto))
  THEN  RepeatFor  3  (PromoteHyp  (-1)  5))

---

Home Index