---

Step * of Lemma run-info_wf

∀[M:Type ⟶ Type]. ∀[r:pRunType(P.M[P])]. ∀[e:runEvents(r)].  (run-info(r;e) ∈ ℤ × Id × pMsg(P.M[P]))
BY
{ (Auto
   THEN D -1
   THEN MoveToConcl (-1)
   THEN D -1
   THEN RepUR ``run-info is-run-event`` 0
   THEN GenConclAtAddr[1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Repeat (Thin (-1))
   THEN D -1
   THEN Reduce 0
   THEN Try (Complete (Auto))) }

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type].  \mforall{}[r:pRunType(P.M[P])].  \mforall{}[e:runEvents(r)].
    (run-info(r;e)  \mmember{}  \mBbbZ{}  \mtimes{}  Id  \mtimes{}  pMsg(P.M[P]))


By

---

Latex:
(Auto
  THEN  D  -1
  THEN  MoveToConcl  (-1)
  THEN  D  -1
  THEN  RepUR  ``run-info  is-run-event``  0
  THEN  GenConclAtAddr[1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Repeat  (Thin  (-1))
  THEN  D  -1
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto)))

---

Home Index