---

Step * 1 of Lemma CLK_ClockFun-eq2


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
⊢ CLK_ClockVal(MsgType;f)@e
= if e ∈b CLK_msg'base(MsgType;f)
    then if first(e)
         then imax(snd(CLK_msg'base(MsgType;f)@e);0) + 1
         else imax(snd(CLK_msg'base(MsgType;f)@e);CLK_ClockVal(MsgType;f)@pred(e)) + 1
         fi 
  if first(e) then 0
  else CLK_ClockVal(MsgType;f)@pred(e)
  fi 
∈ ℤ
BY
{ (UnfoldAtAddr [2] 0
   THEN UnfoldAtAddr [2;2] 0
   THEN (RWO "state-class1-fun-eq" 0 THENA (Auto THEN ProveFunctional THEN Auto))
   THEN Try ((Fold `CLK_Clock` 0 THEN Fold `CLK_ClockFun` 0))
   THEN RepUR ``CLK_upd_clock`` 0
   THEN Repeat (AutoSplit)
   THEN (InstLemma `pair-eta` [⌜CLK_msg'base(MsgType;f)@e⌝]⋅
         THENA (Auto THEN ProveFunctional THEN Auto THEN HypSubst' 3 0 THEN Auto)
         )
   THEN HypSubst' (-1) 0
   THEN Reduce 0
   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
\mvdash{}  CLK\_ClockVal(MsgType;f)@e
=  if  e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f)
        then  if  first(e)
                  then  imax(snd(CLK\_msg'base(MsgType;f)@e);0)  +  1
                  else  imax(snd(CLK\_msg'base(MsgType;f)@e);CLK\_ClockVal(MsgType;f)@pred(e))  +  1
                  fi 
    if  first(e)  then  0
    else  CLK\_ClockVal(MsgType;f)@pred(e)
    fi 


By

---

Latex:
(UnfoldAtAddr  [2]  0
  THEN  UnfoldAtAddr  [2;2]  0
  THEN  (RWO  "state-class1-fun-eq"  0  THENA  (Auto  THEN  ProveFunctional  THEN  Auto))
  THEN  Try  ((Fold  `CLK\_Clock`  0  THEN  Fold  `CLK\_ClockFun`  0))
  THEN  RepUR  ``CLK\_upd\_clock``  0
  THEN  Repeat  (AutoSplit)
  THEN  (InstLemma  `pair-eta`  [\mkleeneopen{}CLK\_msg'base(MsgType;f)@e\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  ProveFunctional  THEN  Auto  THEN  HypSubst'  3  0  THEN  Auto)
              )
  THEN  HypSubst'  (-1)  0
  THEN  Reduce  0
  THEN  Auto
  THEN  ProveFunctional
  THEN  Auto)

---

Home Index