Nuprl Lemma : interface-cmp-zero

[f:Name ─→ Type]. ∀[locs:Id List]. ∀[hdrs:Name List]. ∀[mcmp:hdr:Name ─→ comparison(f hdr)].
[x,y:Interface(to locs, with hdrs)].
  (((interface-cmp(mcmp;locs;hdrs) y) 0 ∈ ℤ)
   {(x.delay y.delay ∈ ℤ)
     ∧ (x.dst y.dst ∈ Id)
     ∧ msg-authentic(x.msg) msg-authentic(y.msg)
     ∧ (msg-header(x.msg) msg-header(y.msg) ∈ Name)
     ∧ ((mcmp msg-header(x.msg) msg-body(x.msg) msg-body(y.msg)) 0 ∈ ℤ)})


Definitions occuring in Statement :  interface-cmp: interface-cmp(mcmp;locs;hdrs) constrained-msg-interface: Interface(to locs, with hdrs) msg-interface-delay: mi.delay msg-interface-message: mi.msg msg-interface-destination: mi.dst msg-body: msg-body(msg) msg-header: msg-header(m) msg-authentic: msg-authentic(m) Id: Id name: Name comparison: comparison(T) list: List bool: 𝔹 uall: [x:A]. B[x] guard: {T} implies:  Q and: P ∧ Q apply: a function: x:A ─→ B[x] natural_number: $n int: universe: Type equal: t ∈ T
Lemmas :  list-index-cmp_wf id-deq_wf msg-interface-destination_wf subtype_rel_comparison l_member_wf msg-header_wf msg-interface-message_wf name-deq_wf compare-fun_wf Message_wf message-cmp_wf equal-wf-T-base interface-cmp_wf comparison_wf constrained-msg-interface_wf name_wf list_wf Id_wf comparison-seq-zero-simple int-minus-comparison_wf msg-interface-delay_wf comparison-seq-simple-wf message-cmp-zero list-index-cmp-zero msg-interface_wf subtype_rel_sets

\mforall{}[f:Name  {}\mrightarrow{}  Type].  \mforall{}[locs:Id  List].  \mforall{}[hdrs:Name  List].  \mforall{}[mcmp:hdr:Name  {}\mrightarrow{}  comparison(f  hdr)].
\mforall{}[x,y:Interface(to  locs,  with  hdrs)].
    (((interface-cmp(mcmp;locs;hdrs)  x  y)  =  0)
    {}\mRightarrow{}  \{(x.delay  =  y.delay)
          \mwedge{}  (x.dst  =  y.dst)
          \mwedge{}  msg-authentic(x.msg)  =  msg-authentic(y.msg)
          \mwedge{}  (msg-header(x.msg)  =  msg-header(y.msg))
          \mwedge{}  ((mcmp  msg-header(x.msg)  msg-body(x.msg)  msg-body(y.msg))  =  0)\})

Date html generated: 2015_07_22-PM-00_01_20
Last ObjectModification: 2015_01_28-AM-08_42_59

Home Index