Nuprl Lemma : CLK_main-opt1

[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 
                                     in let x@0,y@0 
                                        in case name_eq(x@0;``CLK msg``)
                                            of inl(x5) =>
                                            let z,timestamp y@0 
                                            in let x1 ←─ eval timestamp in
                                                         eval clock in
                                                           if (b) < (a)  then 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: a fix: fix(F) lambda: λx.A[x] spread: spread def pair: <a, b> decide: case of inl(x) => s[x] inr(y) => t[y] inr: inr  inl: inl x add: m natural_number: $n token: "$token" sqequal: 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_21
Last ObjectModification: 2015_05_04-PM-06_18_58

Home Index