Nuprl Lemma : CLK_main-program_wf

[MsgType:ValueAllType]. ∀[locs:bag(Id)]. ∀[reply:Id ⟶ MsgType ⟶ (MsgType × Id)]. ∀[f:CLK_headers_type{i:l}(MsgType)].
  (CLK_main-program(MsgType;locs;reply;f) ∈ LocalClass(CLK_main(MsgType;locs;reply;f)))


Proof




Definitions occuring in Statement :  CLK_main-program: CLK_main-program(MsgType;locs;reply;f) CLK_main: CLK_main(MsgType;locs;reply;f) CLK_headers_type: CLK_headers_type{i:l}(MsgType) msg-interface: Interface Message: Message(f) local-class: LocalClass(X) Id: Id vatype: ValueAllType uall: [x:A]. B[x] 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_main: CLK_main(MsgType;locs;reply;f) CLK_main-program: CLK_main-program(MsgType;locs;reply;f) msg-interface: Interface

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\_main-program(MsgType;locs;reply;f)  \mmember{}  LocalClass(CLK\_main(MsgType;locs;reply;f)))



Date html generated: 2016_05_17-PM-02_45_12
Last ObjectModification: 2015_12_29-PM-10_18_59

Theory : lamport!s!clocks


Home Index