---

Step * of Lemma run-event-step-positive

∀[M:Type ─→ Type]
  ∀[S0:System(P.M[P])]. ∀[n2m:ℕ ─→ pMsg(P.M[P])]. ∀[l2m:Id ─→ pMsg(P.M[P])]. ∀[env:pEnvType(P.M[P])].
  ∀[e:runEvents(pRun(S0;env;n2m;l2m))].
    0 < run-event-step(e) 
  supposing Continuous+(P.M[P])
BY
{ (BasicUniformUnivCD Auto
   THEN (Assert pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN Auto⋅
   THEN D -1
   THEN D -2
   THEN RepUR ``run-event-step`` 0
   THEN RepUR ``is-run-event`` -1
   THEN RecUnfold `pRun` (-1)
   THEN Reduce (-1)
   THEN SplitOnHypITE -1 
   THEN Auto') }

1
.....truecase..... 
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. S0 : System(P.M[P])
4. n2m : ℕ ─→ pMsg(P.M[P])
5. l2m : Id ─→ pMsg(P.M[P])
6. env : pEnvType(P.M[P])
7. pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P])
8. e1 : ℕ
9. e2 : Id
10. ↑let info,S = <inr ⋅ , S0> 
     in isl(info) ∧b let ev,z,m = outl(info) in e2 = z
11. e1 = 0 ∈ ℤ
⊢ 0 < e1

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}[S0:System(P.M[P])].  \mforall{}[n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])].  \mforall{}[l2m:Id  {}\mrightarrow{}  pMsg(P.M[P])].
    \mforall{}[env:pEnvType(P.M[P])].  \mforall{}[e:runEvents(pRun(S0;env;n2m;l2m))].
        0  <  run-event-step(e) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(BasicUniformUnivCD  Auto
  THEN  (Assert  pRun(S0;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  Auto\mcdot{}
  THEN  D  -1
  THEN  D  -2
  THEN  RepUR  ``run-event-step``  0
  THEN  RepUR  ``is-run-event``  -1
  THEN  RecUnfold  `pRun`  (-1)
  THEN  Reduce  (-1)
  THEN  SplitOnHypITE  -1 
  THEN  Auto')

---

Home Index