---

Step * of Lemma CLK-msg

∀[MsgType:{T:Type| valueall-type(T)} ]. ∀[locs:bag(Id)]. ∀[reply:Id ⟶ MsgType ⟶ (MsgType × Id)].
∀[f:CLK_headers_type{i:l}(MsgType)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[d:ℤ]. ∀[i:Id]. ∀[auth:𝔹]. ∀[v:MsgType]. ∀[k:ℤ].
  (<d, i, mk-msg(auth;``CLK msg``;<v, k>)> ∈ CLK_main(MsgType;locs;reply;f)(e)
  ⇐⇒ loc(e) ↓∈ locs
      ∧ ((header(e) = ``CLK msg`` ∈ Name) ∧ has-es-info-type(es;e;f;MsgType × ℤ))
      ∧ (d = 0 ∈ ℤ)
      ∧ (i = (snd((reply loc(e) (fst(msgval(e)))))) ∈ Id)
      ∧ auth = ff
      ∧ (v = (fst((reply loc(e) (fst(msgval(e)))))) ∈ MsgType)
      ∧ (k = CLK_ClockVal(MsgType;f)@e ∈ ℤ))
BY
{ ProveILF_instance "msg""CLK" }

---

Latex:

---

Latex:
\mforall{}[MsgType:\{T:Type|  valueall-type(T)\}  ].  \mforall{}[locs:bag(Id)].  \mforall{}[reply:Id  {}\mrightarrow{}  MsgType  {}\mrightarrow{}  (MsgType  \mtimes{}  Id)].
\mforall{}[f:CLK\_headers\_type\{i:l\}(MsgType)].  \mforall{}[es:EO+(Message(f))].  \mforall{}[e:E].  \mforall{}[d:\mBbbZ{}].  \mforall{}[i:Id].  \mforall{}[auth:\mBbbB{}].
\mforall{}[v:MsgType].  \mforall{}[k:\mBbbZ{}].
    (<d,  i,  mk-msg(auth;``CLK  msg``;<v,  k>)>  \mmember{}  CLK\_main(MsgType;locs;reply;f)(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs
            \mwedge{}  ((header(e)  =  ``CLK  msg``)  \mwedge{}  has-es-info-type(es;e;f;MsgType  \mtimes{}  \mBbbZ{}))
            \mwedge{}  (d  =  0)
            \mwedge{}  (i  =  (snd((reply  loc(e)  (fst(msgval(e)))))))
            \mwedge{}  auth  =  ff
            \mwedge{}  (v  =  (fst((reply  loc(e)  (fst(msgval(e)))))))
            \mwedge{}  (k  =  CLK\_ClockVal(MsgType;f)@e))


By

---

Latex:
ProveILF\_instance  "msg""CLK"

---

Home Index