Nuprl Lemma : CLK_msg'send_wf

[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  (CLK_msg'send(MsgType;f) ∈ Id ⟶ (MsgType × ℤ) ⟶ Interface)


Proof




Definitions occuring in Statement :  CLK_msg'send: CLK_msg'send(MsgType;f) CLK_headers_type: CLK_headers_type{i:l}(MsgType) msg-interface: Interface Id: Id vatype: ValueAllType uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] product: x:A × B[x] int:
Definitions unfolded in proof :  vatype: ValueAllType uall: [x:A]. B[x] CLK_headers_type: CLK_headers_type{i:l}(MsgType) l_all: (∀x∈L.P[x]) all: x:A. B[x] and: P ∧ Q member: t ∈ T so_lambda: λ2x.t[x] subtype_rel: A ⊆B prop: so_apply: x[s] iff: ⇐⇒ Q implies:  Q listp: List+ name: Name CLK_headers: CLK_headers() rev_implies:  Q or: P ∨ Q uimplies: supposing a guard: {T} CLK_headers_fun: CLK_headers_fun(MsgType) name_eq: name_eq(x;y) name-deq: NameDeq list-deq: list-deq(eq) list_ind: list_ind cons: [a b] band: p ∧b q ifthenelse: if then else fi  atom-deq: AtomDeq eq_atom: =a y btrue: tt nil: [] it: null: null(as) CLK_msg'send: CLK_msg'send(MsgType;f)

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    (CLK\_msg'send(MsgType;f)  \mmember{}  Id  {}\mrightarrow{}  (MsgType  \mtimes{}  \mBbbZ{})  {}\mrightarrow{}  Interface)



Date html generated: 2016_05_17-PM-02_44_20
Last ObjectModification: 2015_12_29-PM-10_18_36

Theory : lamport!s!clocks


Home Index