Nuprl Lemma : make-msg-interface-equal
∀[f:Name ⟶ Type]. ∀[i1,i2:ℤ]. ∀[l1,l2:Id]. ∀[m1,m2:Message(f)].
(make-msg-interface(i1;l1;m1) = make-msg-interface(i2;l2;m2) ∈ Interface
⇐⇒ (i1 = i2 ∈ ℤ) ∧ (l1 = l2 ∈ Id) ∧ (m1 = m2 ∈ Message(f)))
Proof
Definitions occuring in Statement :
make-msg-interface: make-msg-interface(i;l;m),
msg-interface: Interface,
Message: Message(f),
Id: Id,
name: Name,
uall: ∀[x:A]. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
int: ℤ,
universe: Type,
equal: s = t ∈ T
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
iff: P ⇐⇒ Q,
and: P ∧ Q,
implies: P ⇒ Q,
make-msg-interface: make-msg-interface(i;l;m),
msg-interface: Interface,
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
Latex:
\mforall{}[f:Name {}\mrightarrow{} Type]. \mforall{}[i1,i2:\mBbbZ{}]. \mforall{}[l1,l2:Id]. \mforall{}[m1,m2:Message(f)].
(make-msg-interface(i1;l1;m1) = make-msg-interface(i2;l2;m2)
\mLeftarrow{}{}\mRightarrow{} (i1 = i2) \mwedge{} (l1 = l2) \mwedge{} (m1 = m2))
Date html generated:
2016_05_17-AM-09_00_05
Last ObjectModification:
2016_01_17-PM-08_32_29
Theory : messages
Home
Index