---

Step * 1 of Lemma interface-cmp-zero


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 ∈ ℤ)}
BY
{ (RepUR ``interface-cmp`` -1
   THEN RWO "comparison-seq-zero-simple" (-1)
   THEN Try (BLemma `comparison-seq-simple-wf`)
   THEN Try (QuickAuto)
   THEN D -1
   THEN RWO "comparison-seq-zero-simple" (-1)
   THEN Try (QuickAuto)
   THEN D -1) }

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. (int-minus-comparison(λmi.mi.delay) x y) = 0 ∈ ℤ
11. (list-index-cmp(IdDeq;locs;λmi.mi.dst) x y) = 0 ∈ ℤ
12. (compare-fun(message-cmp(hdrs;mcmp);λmi.mi.msg) 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 ∈ ℤ)}

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  locs  :  Id  List
3.  hdrs  :  Name  List
4.  mcmp  :  hdr:Name  {}\mrightarrow{}  comparison(f  hdr)
5.  list-index-cmp(IdDeq;locs;\mlambda{}mi.mi.dst)  \mmember{}  comparison(Interface(to  locs,  with  hdrs))
6.  list-index-cmp(NameDeq;hdrs;\mlambda{}mi.msg-header(mi.msg))  \mmember{}  comparison(Interface(to  locs,  with  hdrs))
7.  compare-fun(message-cmp(hdrs;mcmp);\mlambda{}mi.mi.msg)  \mmember{}  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
\mvdash{}  \{(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:
(RepUR  ``interface-cmp``  -1
  THEN  RWO  "comparison-seq-zero-simple"  (-1)
  THEN  Try  (BLemma  `comparison-seq-simple-wf`)
  THEN  Try  (QuickAuto)
  THEN  D  -1
  THEN  RWO  "comparison-seq-zero-simple"  (-1)
  THEN  Try  (QuickAuto)
  THEN  D  -1)

---

Home Index