Nuprl Lemma : interface-cmp-zero
∀[f:Name ─→ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)].
∀[x,y:Interface(to locs, with hdrs)].
(((interface-cmp(mcmp;locs;hdrs) x y) = 0 ∈ ℤ)
⇒ {(x.delay = y.delay ∈ ℤ)
∧ (x.dst = y.dst ∈ Id)
∧ msg-authentic(x.msg) = msg-authentic(y.msg)
∧ (msg-header(x.msg) = msg-header(y.msg) ∈ Name)
∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0 ∈ ℤ)})
Proof
Definitions occuring in Statement :
interface-cmp: interface-cmp(mcmp;locs;hdrs),
constrained-msg-interface: Interface(to locs, with hdrs),
msg-interface-delay: mi.delay,
msg-interface-message: mi.msg,
msg-interface-destination: mi.dst,
msg-body: msg-body(msg),
msg-header: msg-header(m),
msg-authentic: msg-authentic(m),
Id: Id,
name: Name,
comparison: comparison(T),
list: T List,
bool: 𝔹,
uall: ∀[x:A]. B[x],
guard: {T},
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
natural_number: $n,
int: ℤ,
universe: Type,
equal: s = t ∈ T
Lemmas :
list-index-cmp_wf,
id-deq_wf,
msg-interface-destination_wf,
subtype_rel_comparison,
l_member_wf,
msg-header_wf,
msg-interface-message_wf,
name-deq_wf,
compare-fun_wf,
Message_wf,
message-cmp_wf,
equal-wf-T-base,
interface-cmp_wf,
comparison_wf,
constrained-msg-interface_wf,
name_wf,
list_wf,
Id_wf,
comparison-seq-zero-simple,
int-minus-comparison_wf,
msg-interface-delay_wf,
comparison-seq-simple-wf,
message-cmp-zero,
list-index-cmp-zero,
msg-interface_wf,
subtype_rel_sets
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[locs:Id List]. \mforall{}[hdrs:Name List]. \mforall{}[mcmp:hdr:Name {}\mrightarrow{} comparison(f hdr)].
\mforall{}[x,y:Interface(to locs, with hdrs)].
(((interface-cmp(mcmp;locs;hdrs) x y) = 0)
{}\mRightarrow{} \{(x.delay = y.delay)
\mwedge{} (x.dst = y.dst)
\mwedge{} msg-authentic(x.msg) = msg-authentic(y.msg)
\mwedge{} (msg-header(x.msg) = msg-header(y.msg))
\mwedge{} ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) = 0)\})
Date html generated:
2015_07_22-PM-00_01_20
Last ObjectModification:
2015_01_28-AM-08_42_59
Home
Index