---

Step * of 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 ⋅ )
BY
{ (RepUR ``eq_atom btrue bfalse hdf-halt`` 0 THEN SqequalProcProve2) }

---

Latex:

---

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{}  )


By

---

Latex:
(RepUR  ``eq\_atom  btrue  bfalse  hdf-halt``  0  THEN  SqequalProcProve2)

---

Home Index