Nuprl Lemma : CLK_message-constraint_wf

[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ⟶ MsgType ⟶ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  (CLK_message-constraint{i:l}(MsgType;locs;reply;f) ∈ ℙ')


Proof




Definitions occuring in Statement :  CLK_message-constraint: CLK_message-constraint{i:l}(MsgType;locs;reply;f) CLK_headers_type: CLK_headers_type{i:l}(MsgType) Id: Id vatype: ValueAllType uall: [x:A]. B[x] prop: member: t ∈ T function: x:A ⟶ B[x] product: x:A × B[x] bag: bag(T)
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_message-constraint: CLK_message-constraint{i:l}(MsgType;locs;reply;f)

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[locs:bag(Id)].  \mforall{}[reply:Id  {}\mrightarrow{}  MsgType  {}\mrightarrow{}  (MsgType  \mtimes{}  Id)].
\mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].
    (CLK\_message-constraint\{i:l\}(MsgType;locs;reply;f)  \mmember{}  \mBbbP{}')



Date html generated: 2016_05_17-PM-02_45_33
Last ObjectModification: 2015_12_29-PM-10_18_26

Theory : lamport!s!clocks


Home Index