Nuprl Lemma : CLK-prop2

MsgType:ValueAllType. ∀locs:bag(Id). ∀reply:Id ⟶ MsgType ⟶ (MsgType × Id). ∀f:CLK_headers_type{i:l}(MsgType).
es:EO+(Message(f)). ∀e1,e2:E. ∀clock1,clock2:ℤ.
  ((∀e:E. (↑e ∈b CLK_msg'base(MsgType;f)))
   e1 ⟶ e2
   clock1 ∈ CLK_Clock(MsgType;f)(e1)
   clock2 ∈ CLK_Clock(MsgType;f)(e2)
   clock1 < clock2)


Proof




Definitions occuring in Statement :  CLK_main: CLK_main(MsgType;locs;reply;f) CLK_Clock: CLK_Clock(MsgType;f) CLK_msg'base: CLK_msg'base(MsgType;f) CLK_headers_type: CLK_headers_type{i:l}(MsgType) es-happened-before: e1 ⟶ e2 Message: Message(f) classrel: v ∈ X(e) member-eclass: e ∈b X event-ordering+: EO+(Info) es-E: E Id: Id vatype: ValueAllType assert: b less_than: a < b all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] product: x:A × B[x] int: bag: bag(T)
Definitions unfolded in proof :  vatype: ValueAllType all: x:A. B[x] implies:  Q CLK_headers_type: CLK_headers_type{i:l}(MsgType) l_all: (∀x∈L.P[x]) and: P ∧ Q member: t ∈ T uall: [x:A]. B[x] so_lambda: λ2x.t[x] subtype_rel: A ⊆B prop: so_apply: x[s] iff: ⇐⇒ Q listp: List+ name: Name int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A less_than: a < b squash: T length: ||as|| list_ind: list_ind CLK_headers: CLK_headers() cons: [a b] nil: [] it: true: True select: L[n] uimplies: supposing a guard: {T} rev_implies:  Q CLK_headers_fun: CLK_headers_fun(MsgType) name_eq: name_eq(x;y) name-deq: NameDeq list-deq: list-deq(eq) band: p ∧b q ifthenelse: if then else fi  atom-deq: AtomDeq eq_atom: =a y btrue: tt null: null(as) strongwellfounded: SWellFounded(R[x; y]) exists: x:A. B[x] nat: ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top decidable: Dec(P) or: P ∨ Q es-happened-before: e1 ⟶ e2 event-caused-by: e2 caused by e1 in S cand: c∧ B es-locl: (e <loc e') label: ...$L... t make-msg-interface: make-msg-interface(i;l;m) has-es-info-type: has-es-info-type(es;e;f;T) sq_type: SQType(T) bool: 𝔹 unit: Unit uiff: uiff(P;Q) CLK_msg'base: CLK_msg'base(MsgType;f) es-info-body: msgval(e) make-Msg: make-Msg(hdr;val) make-Authentic-Msg: make-Authentic-Msg(hdr;val) Message: Message(f) pi1: fst(t) pi2: snd(t) bfalse: ff msg-type: msg-type(msg;f) msg-has-type: msg-has-type(m;f;T) sq_stable: SqStable(P) encodes-msg-type: hdr encodes T bnot: ¬bb assert: b

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).  \mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.  \mforall{}clock1,clock2:\mBbbZ{}.
    ((\mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f)))
    {}\mRightarrow{}  e1  {}\mrightarrow{}  e2
    {}\mRightarrow{}  clock1  \mmember{}  CLK\_Clock(MsgType;f)(e1)
    {}\mRightarrow{}  clock2  \mmember{}  CLK\_Clock(MsgType;f)(e2)
    {}\mRightarrow{}  clock1  <  clock2)



Date html generated: 2016_05_17-PM-02_46_27
Last ObjectModification: 2016_01_18-AM-09_50_33

Theory : lamport!s!clocks


Home Index