### Nuprl Lemma : message-cmp-zero

`∀[f:Name ─→ Type]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)]. ∀[x,y:{m:Message(f)| `
`                                                                                    (msg-header(m) ∈ hdrs)} ].`
`  uiff((message-cmp(hdrs;mcmp) x y) = 0 ∈ ℤ;msg-authentic(x) = msg-authentic(y)`
`  ∧ (msg-header(x) = msg-header(y) ∈ Name)`
`  ∧ ((mcmp msg-header(x) msg-body(x) msg-body(y)) = 0 ∈ ℤ))`

Proof

Definitions occuring in Statement :  message-cmp: `message-cmp(hdrs;mcmp)` msg-body: `msg-body(msg)` msg-header: `msg-header(m)` msg-authentic: `msg-authentic(m)` Message: `Message(f)` name: `Name` comparison: `comparison(T)` l_member: `(x ∈ l)` list: `T List` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` and: `P ∧ Q` set: `{x:A| B[x]} ` apply: `f a` function: `x:A ─→ B[x]` natural_number: `\$n` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Lemmas :  equal-wf-T-base message-cmp_wf comparison_wf bool_wf msg-authentic_wf msg-header_wf msg-body_wf2 msg-type_wf subtype_rel-equal iff_weakening_equal set_wf Message_wf l_member_wf list_wf name_wf comparison-seq-zero compare-fun_wf bool-cmp_wf comparison-seq_wf list-index-cmp_wf name-deq_wf subtype_rel_comparison msg-body-cmp_wf subtype_rel_nested_set2 subtype_rel_nested_set subtype_rel_sets list-index-cmp-zero bool-cmp-zero iff_transitivity iff_weakening_uiff

Latex:
\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].  \mforall{}[x,y:\{m:Message(f)|