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:
(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