### 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`
Lemmas :  iff_imp_equal_bool assert_elim subtype_base_sq bool_wf bool_subtype_base assert_wf and_wf equal_wf name_wf pi1_wf_top subtype_rel_product top_wf subtype_top Message_wf mk-msg_wf subtype_rel_self subtype_rel_wf list_subtype_base atom_subtype_base

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: 2015_07_21-PM-04_53_20
Last ObjectModification: 2015_01_28-AM-08_44_48

Home Index