---

Step * of Lemma CLK_ClockFun-eq

∀[MsgType:ValueAllType]. ∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E].
  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)
  ∈ ℤ 
  supposing ∀e:E. (↑e ∈b CLK_msg'base(MsgType;f))
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
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)
∈ ℤ

---

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
    =  (imax(snd(CLK\_msg'base(MsgType;f)@e);if  first(e)
                    then  0
                    else  CLK\_ClockVal(MsgType;f)@pred(e)
                    fi  )
        +  1) 
    supposing  \mforall{}e:E.  (\muparrow{}e  \mmember{}\msubb{}  CLK\_msg'base(MsgType;f))


By

---

Latex:
StartEmlProof

---

Home Index