---

Step * 2 2 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. msg-authentic(x) = msg-authentic(y)
7. msg-header(x) = msg-header(y) ∈ Name
8. (mcmp msg-header(x) msg-body(x) msg-body(y)) = 0 ∈ ℤ
9. a : {m:Message(f)| (msg-header(m) ∈ hdrs)} 
10. a@0 : {b:{m:Message(f)| (msg-header(m) ∈ hdrs)} | (compare-fun(bool-cmp();λm.msg-authentic(m)) a b) = 0 ∈ ℤ} 
⊢ msg-body-cmp(mcmp) ∈ comparison({b:{b:{m:Message(f)| (msg-header(m) ∈ hdrs)} | 
                                      (compare-fun(bool-cmp();λm.msg-authentic(m)) a b) = 0 ∈ ℤ} | 
                                   (list-index-cmp(NameDeq;hdrs;λm.msg-header(m)) a@0 b) = 0 ∈ ℤ} )
BY
{ (InstLemma `msg-body-cmp_wf` [⌜f⌝;⌜hdrs⌝;⌜mcmp⌝;⌜a@0⌝]⋅ THEN Auto) }

---

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.  msg-authentic(x)  =  msg-authentic(y)
7.  msg-header(x)  =  msg-header(y)
8.  (mcmp  msg-header(x)  msg-body(x)  msg-body(y))  =  0
9.  a  :  \{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\} 
10.  a@0  :  \{b:\{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\}  | 
                      (compare-fun(bool-cmp();\mlambda{}m.msg-authentic(m))  a  b)  =  0\} 
\mvdash{}  msg-body-cmp(mcmp)  \mmember{}  comparison(\{b:\{b:\{m:Message(f)|  (msg-header(m)  \mmember{}  hdrs)\}  | 
                                                                            (compare-fun(bool-cmp();\mlambda{}m.msg-authentic(m))  a  b)  =  0\}  | 
                                                                      (list-index-cmp(NameDeq;hdrs;\mlambda{}m.msg-header(m))  a@0  b)  =  0\}  )


By

---

Latex:
(InstLemma  `msg-body-cmp\_wf`  [\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}hdrs\mkleeneclose{};\mkleeneopen{}mcmp\mkleeneclose{};\mkleeneopen{}a@0\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index