Nuprl Lemma : make-Msg-equal
∀[f:Name ⟶ Type]. ∀[hdr1,hdr2:Name]. ∀[val1:f hdr1]. ∀[val2:f hdr2].
(make-Msg(hdr1;val1) = make-Msg(hdr2;val2) ∈ Message(f) ⇐⇒ {(hdr1 = hdr2 ∈ Name) ∧ (val1 = val2 ∈ (f hdr1))})
Proof
Definitions occuring in Statement :
make-Msg: make-Msg(hdr;val),
Message: Message(f),
name: Name,
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,
make-Msg: make-Msg(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),
pi2: snd(t),
prop: ℙ,
rev_implies: P ⇐ Q,
squash: ↓T,
true: True,
name: Name,
sq_type: SQType(T)
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[hdr1,hdr2:Name]. \mforall{}[val1:f hdr1]. \mforall{}[val2:f hdr2].
(make-Msg(hdr1;val1) = make-Msg(hdr2;val2) \mLeftarrow{}{}\mRightarrow{} \{(hdr1 = hdr2) \mwedge{} (val1 = val2)\})
Date html generated:
2016_05_17-AM-08_57_45
Last ObjectModification:
2016_01_17-PM-08_32_42
Theory : messages
Home
Index