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
Lemmas :
and_wf,
equal_wf,
Id_wf,
Message_wf,
pi1_wf_top,
subtype_rel_product,
top_wf,
subtype_top,
pi2_wf,
msg-interface_wf,
make-msg-interface_wf,
equal-wf-base,
int_subtype_base
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:
2015_07_22-AM-11_59_22
Last ObjectModification:
2015_01_28-AM-08_41_51
Home
Index