Nuprl Lemma : Message-extensionality
∀[f:Name ─→ Type]. ∀[m1,m2:Message(f)].
uiff(m1 = m2 ∈ Message(f);msg-authentic(m1) = msg-authentic(m2)
∧ (msg-header(m1) = msg-header(m2) ∈ Name)
∧ (msg-body(m1) = msg-body(m2) ∈ (f msg-header(m1))))
Proof
Definitions occuring in Statement :
msg-body: msg-body(msg),
msg-header: msg-header(m),
msg-authentic: msg-authentic(m),
Message: Message(f),
name: Name,
bool: 𝔹,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
and: P ∧ Q,
apply: f a,
function: x:A ─→ B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
iff_imp_equal_bool,
msg-authentic_wf,
and_wf,
equal_wf,
Message_wf,
assert_elim,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_wf,
msg-header_wf,
msg-body_wf2,
subtype_rel_self,
msg-type_wf,
subtype_rel_wf,
name_wf,
subtype_rel-equal,
iff_weakening_equal
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[m1,m2:Message(f)].
uiff(m1 = m2;msg-authentic(m1) = msg-authentic(m2)
\mwedge{} (msg-header(m1) = msg-header(m2))
\mwedge{} (msg-body(m1) = msg-body(m2)))
Date html generated:
2015_07_21-PM-04_48_27
Last ObjectModification:
2015_02_04-PM-05_09_20
Home
Index