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