---

Step * 1 of Lemma message-cmp-zero


1. f : Name ⟶ Type
2. hdrs : Name List
3. mcmp : hdr:Name ⟶ comparison(f hdr)
4. x : {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. y : {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. (message-cmp(hdrs;mcmp) x y) = 0 ∈ ℤ
⊢ msg-authentic(x) = msg-authentic(y)
∧ (msg-header(x) = msg-header(y) ∈ Name)
∧ ((mcmp msg-header(x) msg-body(x) msg-body(y)) = 0 ∈ ℤ)
BY
{ (RepUR ``message-cmp`` -1
   THEN (RWO "comparison-seq-zero" (-1)
         THENA (Auto THEN RenameVar `xx' (-1) THEN InstLemma `msg-body-cmp_wf` [⌜f⌝;⌜hdrs⌝;⌜mcmp⌝;⌜xx⌝]⋅ THEN Auto)
         )
   THEN D -1
   THEN RWO "comparison-seq-zero" (-1)
   THEN Auto
   THEN ∀h:hyp. (RWO "list-index-cmp-zero" h THEN Auto) ) }

1
1. f : Name ⟶ Type
2. hdrs : Name List
3. mcmp : hdr:Name ⟶ comparison(f hdr)
4. x : {m:Message(f)| (msg-header(m) ∈ hdrs)} 
5. y : {m:Message(f)| (msg-header(m) ∈ hdrs)} 
6. (compare-fun(bool-cmp();λm.msg-authentic(m)) x y) = 0 ∈ ℤ
7. ((λm.msg-header(m)) x) = ((λm.msg-header(m)) y) ∈ Name
8. (msg-body-cmp(mcmp) x y) = 0 ∈ ℤ
⊢ msg-authentic(x) = msg-authentic(y)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  hdrs  :  Name  List
3.  mcmp  :  hdr:Name  {}\mrightarrow{}  comparison(f  hdr)
4.  x  :  \{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\} 
5.  y  :  \{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\} 
6.  (message-cmp(hdrs;mcmp)  x  y)  =  0
\mvdash{}  msg-authentic(x)  =  msg-authentic(y)
\mwedge{}  (msg-header(x)  =  msg-header(y))
\mwedge{}  ((mcmp  msg-header(x)  msg-body(x)  msg-body(y))  =  0)


By

---

Latex:
(RepUR  ``message-cmp``  -1
  THEN  (RWO  "comparison-seq-zero"  (-1)
              THENA  (Auto
                            THEN  RenameVar  `xx'  (-1)
                            THEN  InstLemma  `msg-body-cmp\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}hdrs\mkleeneclose{};\mkleeneopen{}mcmp\mkleeneclose{};\mkleeneopen{}xx\mkleeneclose{}]\mcdot{}
                            THEN  Auto)
              )
  THEN  D  -1
  THEN  RWO  "comparison-seq-zero"  (-1)
  THEN  Auto
  THEN  \mforall{}h:hyp.  (RWO  "list-index-cmp-zero"  h  THEN  Auto)  )

---

Home Index