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
Lemmas :  hdf-state-base,  hdf-base-transformation1,  hdf-compose1-transformation2,  false_wf,  le_wf,  hdf-compose2-transformation2,  lifting-strict-less,  has-value-ifthenelse-type,  has-value_wf_base,  base_wf,  base_sq,  lifting-strict-int_eq,  lifting-strict-spread,  strict4-spread,  lifting-strict-callbyvalue,  value-type-has-value,  int-value-type,  lifting-strict-ifthenelse,  mk_lambdas_unroll_ite,  mk_lambdas_fun-unroll-ite,  lifting-callbyvalueall-decide-name_eq,  lifting-callbyvalueall-spread,  map-decide,  map_cons_lemma,  name_eq_spread,  decide-spread,  map_nil_lemma,  normalization-spread3,  normalize-decide-left,  normalize-decide-right,  bag_combine_empty_lemma,  bag-combine-unit-left-top,  bag-combine-append-empty,  top_wf
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: 2015_07_23-PM-04_10_23
Last ObjectModification: 2015_05_04-PM-06_18_56

Home Index