Nuprl 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 ∈ ℤ))
Proof
Definitions occuring in Statement :
message-cmp: message-cmp(hdrs;mcmp),
msg-body: msg-body(msg),
msg-header: msg-header(m),
msg-authentic: msg-authentic(m),
Message: Message(f),
name: Name,
comparison: comparison(T),
l_member: (x ∈ l),
list: T List,
bool: 𝔹,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
equal-wf-T-base,
message-cmp_wf,
comparison_wf,
bool_wf,
msg-authentic_wf,
msg-header_wf,
msg-body_wf2,
msg-type_wf,
subtype_rel-equal,
iff_weakening_equal,
set_wf,
Message_wf,
l_member_wf,
list_wf,
name_wf,
comparison-seq-zero,
compare-fun_wf,
bool-cmp_wf,
comparison-seq_wf,
list-index-cmp_wf,
name-deq_wf,
subtype_rel_comparison,
msg-body-cmp_wf,
subtype_rel_nested_set2,
subtype_rel_nested_set,
subtype_rel_sets,
list-index-cmp-zero,
bool-cmp-zero,
iff_transitivity,
iff_weakening_uiff
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))
Date html generated:
2015_07_22-PM-00_01_14
Last ObjectModification:
2015_02_04-PM-05_09_07
Home
Index