---

Step * 1 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. (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)
BY
{ RepUR ``compare-fun`` -3 }

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. (bool-cmp() msg-authentic(x) msg-authentic(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.  (compare-fun(bool-cmp();\mlambda{}m.msg-authentic(m))  x  y)  =  0
7.  ((\mlambda{}m.msg-header(m))  x)  =  ((\mlambda{}m.msg-header(m))  y)
8.  (msg-body-cmp(mcmp)  x  y)  =  0
\mvdash{}  msg-authentic(x)  =  msg-authentic(y)


By

---

Latex:
RepUR  ``compare-fun``  -3

---

Home Index