---

Step * of Lemma message-cmp-zero

∀[f:Name ─→ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)]. ∀[x,y:{m:Message(f)| 
                                                                                    (msg-header(m) ∈ hdrs)} ].
  uiff((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
{ (Intros THEN (RepeatFor 2 (D 0) THENA 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. (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 ∈ ℤ)

2
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)
∧ (msg-header(x) = msg-header(y) ∈ Name)
∧ ((mcmp msg-header(x) msg-body(x) msg-body(y)) = 0 ∈ ℤ)
⊢ (message-cmp(hdrs;mcmp) x y) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].  \mforall{}[x,y:\{m:Message(f)| 
                                                                                                                                                                        (msg-header(m)
                                                                                                                                                                            \mmember{}  hdrs)\}  ].
    uiff((message-cmp(hdrs;mcmp)  x  y)  =  0;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:
(Intros  THEN  (RepeatFor  2  (D  0)  THENA  Auto))

---

Home Index