---

Step * of Lemma CLK_ClockFun-eq2

∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[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
{ StartEmlProof }

1
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 
∈ ℤ

---

Latex:

---

Latex:
\mforall{}[MsgType:ValueAllType].  \mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].
    (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:
StartEmlProof

---

Home Index