---

Step * of Lemma CLK-ilf

∀[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]. ∀[m:Message(f)].
  {<d, i, m> ∈ 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)
      ∧ (m = make-Msg(``CLK msg``;<fst((reply loc(e) (fst(msgval(e))))), CLK_ClockVal(MsgType;f)@e>) ∈ Message(f))}
BY
{ ProveILF_lemma clock.esh }

---

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{}[m:Message(f)].
    \{<d,  i,  m>  \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{}  (m  =  make-Msg(``CLK  msg``;<fst((reply  loc(e)  (fst(msgval(e))))),  CLK\_ClockVal(MsgType;f)@e>)\000C)\}


By

---

Latex:
ProveILF\_lemma  clock.esh

---

Home Index