Nuprl Lemma : CLK_main-opt2

∀[MsgType,locs,reply,f:Top].
  (CLK_main-program(MsgType;locs;reply;f) 
  ~ λi.case i ∈b locs
        of inl() =>
        fix((λmk-hdf,clock. (inl (λv.let x,y = v 
                                     in let x@0,y@0 = y 
                                        in case name_eq(x@0;``CLK msg``)
                                            of inl(x5) =>
                                            let z,timestamp = y@0 
                                            in let x1 ⟵ eval a = timestamp in
                                                         eval b = clock in
                                                           if (b) < (a)  then a + 1  else (b + 1)
                                               in let v3 ⟵ (CLK_mk_reply(MsgType;reply;f) i <z, timestamp> x1) @ []
                                                  in <mk-hdf x1, v3>
                                            | inr(x5) =>
                                            let x2 ⟵ clock
                                            in <mk-hdf x2, []>)))) 
        0
        | inr() =>
        inr ⋅ )


Proof



Definitions occuring in Statement :  CLK_main-program: CLK_main-program(MsgType;locs;reply;f),  CLK_mk_reply: CLK_mk_reply(MsgType;reply;f),  name_eq: name_eq(x;y),  deq-member: x ∈b L,  append: as @ bs,  cons: [a / b],  nil: [],  callbyvalueall: callbyvalueall,  callbyvalue: callbyvalue,  atom_eq: atomeqn def,  it: ⋅,  uall: ∀[x:A]. B[x],  top: Top,  less: if (a) < (b)  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n,  token: "$token",  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  CLK_main-program: CLK_main-program(MsgType;locs;reply;f),  CLK_Reply-program: CLK_Reply-program(MsgType;reply;f),  class-at-program: (pr)@locs,  id-deq: IdDeq,  bag-deq-member: bag-deq-member(eq;x;b),  CLK_msg'base-program: CLK_msg'base-program(MsgType;f),  eclass1-program: eclass1-program(f;pr),  CLK_Clock-program: CLK_Clock-program(MsgType;f),  eclass2-program: Xpr o Ypr,  hdf-halt: hdf-halt(),  atom2-deq: Atom2Deq,  base-class-program: base-class-program(hdr),  state-class1-program: state-class1-program(init;tr;pr),  eq_atom: eq_atom$n(x;y),  single-bag: {x},  loop-class-state-program: loop-class-state-program(pr;init),  btrue: tt,  bfalse: ff,  cond-msg-body: cond-msg-body(hdr;msg),  empty-bag: {},  msg-header: msg-header(m),  CLK_upd_clock: CLK_upd_clock(MsgType),  so_lambda: λ2x y.t[x; y],  top: Top,  so_apply: x[s1;s2],  so_lambda: λ2x.t[x],  so_apply: x[s],  nat: ℕ,  le: A ≤ B,  and: P ∧ Q,  less_than': less_than'(a;b),  false: False,  not: ¬A,  implies: P ⇒ Q,  prop: ℙ,  lt_int: i <z j,  eq_int: (i =z j),  msg-msg: msg-msg(m),  pi1: fst(t),  msg-body: msg-body(msg),  bag-map: bag-map(f;bs),  bottom: ⊥,  imax: imax(a;b),  subtract: n - m,  pi2: snd(t),  le_int: i ≤z j,  bnot: ¬bb,  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  so_apply: x[s1;s2;s3;s4],  uimplies: b supposing a,  strict4: strict4(F),  all: ∀x:A. B[x],  has-value: (a)↓,  ifthenelse: if b then t else f fi ,  guard: {T},  or: P ∨ Q,  squash: ↓T,  cbva_seq: cbva_seq(L; F; m),  select_fun_last: select_fun_last(g;m),  select_fun_ap: select_fun_ap(g;n;m),  partial_ap_gen: partial_ap_gen(g;n;s;m),  callbyvalueall_seq: callbyvalueall_seq(L;G;F;n;m),  bag-append: as + bs,  callbyvalueall: callbyvalueall,  evalall: evalall(t),  cons: [a / b],  CLK_mk_reply: CLK_mk_reply(MsgType;reply;f),  map: map(f;as),  list_ind: list_ind,  nil: [],  it: ⋅,  bag-combine: ⋃x∈bs.f[x],  bag-union: bag-union(bbs),  concat: concat(ll),  reduce: reduce(f;k;as)
Latex:
\mforall{}[MsgType,locs,reply,f:Top].
    (CLK\_main-program(MsgType;locs;reply;f) 
    \msim{}  \mlambda{}i.case  i  \mmember{}\msubb{}  locs
                of  inl()  =>
                fix((\mlambda{}mk-hdf,clock.  (inl  (\mlambda{}v.let  x,y  =  v 
                                                                          in  let  x@0,y@0  =  y 
                                                                                in  case  name\_eq(x@0;``CLK  msg``)
                                                                                        of  inl(x5)  =>
                                                                                        let  z,timestamp  =  y@0 
                                                                                        in  let  x1  \mleftarrow{}{}  eval  a  =  timestamp  in
                                                                                                                  eval  b  =  clock  in
                                                                                                                      if  (b)  <  (a)    then  a  +  1    else  (b  +  1)
                                                                                              in  let  v3  \mleftarrow{}{}  (CLK\_mk\_reply(MsgType;reply;f)  i 
                                                                                                                          <z,  timestamp> 
                                                                                                                          x1)
                                                                                                    @  []
                                                                                                    in  <mk-hdf  x1,  v3>
                                                                                        |  inr(x5)  =>
                                                                                        let  x2  \mleftarrow{}{}  clock
                                                                                        in  <mk-hdf  x2,  []>)))) 
                0
                |  inr()  =>
                inr  \mcdot{}  )


Date html generated: 2016_05_17-PM-02_46_00
Last ObjectModification: 2016_01_18-AM-09_50_28

Theory : lamport!s!clocks


Home Index