Nuprl Lemma : mk-msg-equal
∀[f:Name ⟶ Type]. ∀[auth1,auth2:𝔹]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
(mk-msg(auth1;hdr1;val1) = mk-msg(auth2;hdr2;val2) ∈ Message(f)
⇐⇒ {auth1 = auth2 ∧ (hdr1 = hdr2 ∈ Name) ∧ (val1 = val2 ∈ (f hdr1))})
Proof
Definitions occuring in Statement :
mk-msg: mk-msg(auth;hdr;val),
Message: Message(f),
name: Name,
bool: 𝔹,
uall: ∀[x:A]. B[x],
guard: {T},
iff: P ⇐⇒ Q,
and: P ∧ Q,
apply: f a,
function: x:A ⟶ B[x],
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
guard: {T},
uall: ∀[x:A]. B[x],
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
mk-msg: mk-msg(auth;hdr;val),
Message: Message(f),
make-basicMsg: make-basicMsg(hdr;val),
basicMessage: basicMessage(f),
so_lambda: λ2x.t[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
uimplies: b supposing a,
all: ∀x:A. B[x],
top: Top,
pi1: fst(t),
sq_type: SQType(T),
assert: ↑b,
ifthenelse: if b then t else f fi ,
btrue: tt,
true: True,
prop: ℙ,
rev_implies: P ⇐ Q,
pi2: snd(t),
squash: ↓T,
name: Name
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[auth1,auth2:\mBbbB{}]. \mforall{}[hdr1,hdr2:Name]. \mforall{}[val1:f hdr1]. \mforall{}[val2:f hdr2].
(mk-msg(auth1;hdr1;val1) = mk-msg(auth2;hdr2;val2)
\mLeftarrow{}{}\mRightarrow{} \{auth1 = auth2 \mwedge{} (hdr1 = hdr2) \mwedge{} (val1 = val2)\})
Date html generated:
2016_05_17-AM-08_57_33
Last ObjectModification:
2016_01_17-PM-08_32_49
Theory : messages
Home
Index