---

Step * 1 of Lemma CLK_ClockFun-eq


1. MsgType : {T:Type| valueall-type(T)} 
2. f : CLK_headers_type{i:l}(MsgType)
3. (f ``CLK msg``) = (MsgType × ℤ) ∈ Type
4. f ∈ Name ⟶ Type
5. es : EO+(Message(f))
6. e : E
7. ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))
⊢ CLK_ClockVal(MsgType;f)@e
= (imax(snd(CLK_msg'base(MsgType;f)@e);if first(e) then 0 else CLK_ClockVal(MsgType;f)@pred(e) fi ) + 1)
∈ ℤ
BY
{ (RepUR ``CLK_ClockFun CLK_Clock state-class1`` 0
   THEN RW (AddrC [2] (LemmaC `loop-class-state-fun-eq`)) 0
   THEN Reduce 0
   THEN Auto
   THEN (ProveFunctional THEN Auto)
   THEN Reduce 0
   THEN Repeat (AutoSplit)
   THEN Try ((RWO "classfun-res-eclass1" 0 THENA Auto))
   THEN (ProveFunctional THEN Auto)
   THEN Try (Complete ((D (-3) THEN RWO "member-eclass-eclass1" 0 THEN Auto)))
   THEN Try (Complete ((D (-2) THEN RWO "member-eclass-eclass1" 0 THEN Auto)))
   THEN RepUR ``CLK_upd_clock`` 0
   THEN GenConclAtAddr [2;1]
   THEN Try (DProdsAndUnions)
   THEN AllReduce
   THEN Auto
   THEN ProveFunctional
   THEN Auto) }

---

Latex:

---

Latex:

1.  MsgType  :  \{T:Type|  valueall-type(T)\} 
2.  f  :  CLK\_headers\_type\{i:l\}(MsgType)
3.  (f  ``CLK  msg``)  =  (MsgType  \mtimes{}  \mBbbZ{})
4.  f  \mmember{}  Name  {}\mrightarrow{}  Type
5.  es  :  EO+(Message(f))
6.  e  :  E
7.  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f))
\mvdash{}  CLK\_ClockVal(MsgType;f)@e
=  (imax(snd(CLK\_msg'base(MsgType;f)@e);if  first(e)  then  0  else  CLK\_ClockVal(MsgType;f)@pred(e)  fi  )
    +  1)


By

---

Latex:
(RepUR  ``CLK\_ClockFun  CLK\_Clock  state-class1``  0
  THEN  RW  (AddrC  [2]  (LemmaC  `loop-class-state-fun-eq`))  0
  THEN  Reduce  0
  THEN  Auto
  THEN  (ProveFunctional  THEN  Auto)
  THEN  Reduce  0
  THEN  Repeat  (AutoSplit)
  THEN  Try  ((RWO  "classfun-res-eclass1"  0  THENA  Auto))
  THEN  (ProveFunctional  THEN  Auto)
  THEN  Try  (Complete  ((D  (-3)  THEN  RWO  "member-eclass-eclass1"  0  THEN  Auto)))
  THEN  Try  (Complete  ((D  (-2)  THEN  RWO  "member-eclass-eclass1"  0  THEN  Auto)))
  THEN  RepUR  ``CLK\_upd\_clock``  0
  THEN  GenConclAtAddr  [2;1]
  THEN  Try  (DProdsAndUnions)
  THEN  AllReduce
  THEN  Auto
  THEN  ProveFunctional
  THEN  Auto)

---

Home Index