---

Step * of Lemma pRun-invariant2

∀[M:Type ─→ Type]
  ∀n2m:ℕ ─→ pMsg(P.M[P]). ∀l2m:Id ─→ pMsg(P.M[P]). ∀S0:System(P.M[P]). ∀env:pEnvType(P.M[P]).
    let r = pRun(S0;env;n2m;l2m) in
        ∀e1,e2:runEvents(r).
          (∀P:Process(P.M[P])
             ((P ∈ run-prior-state(S0;r;e1))
             ⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)))
                  ∈ run-event-state(r;e2)))) supposing 
             ((run-event-step(e1) ≤ run-event-step(e2)) and 
             (run-event-loc(e1) = run-event-loc(e2) ∈ Id)) 
  supposing Continuous+(P.M[P])
BY
{ (InstLemma `run-event-state-next` []
   THEN RepeatFor 6 ((ParallelLast' THENA Auto))
   THEN MoveToConcl (-1)
   THEN GenConclAtAddr [1;1]
   THEN RenameVar `r' (-2)
   THEN RepUR ``let`` 0
   THEN (Assert r ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN (D 0 THENA Auto)) }

1
1. [M] : Type ─→ Type
2. Continuous+(P.M[P])
3. n2m : ℕ ─→ pMsg(P.M[P])@i
4. l2m : Id ─→ pMsg(P.M[P])@i
5. S0 : System(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. r : fulpRunType(P.M[P])@i
8. pRun(S0;env;n2m;l2m) = r ∈ fulpRunType(P.M[P])@i
9. r ∈ pRunType(P.M[P])
10. ∀e:runEvents(r)
      sub-mset(Process(P.M[P]); map(λP.(fst(Process-apply(P;run-event-msg(r;e))));run-prior-state(S0;r;e));
               run-event-state(r;e))@i
⊢ ∀e1,e2:runEvents(r).
    (∀P:Process(P.M[P])
       ((P ∈ run-prior-state(S0;r;e1))
       ⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)))
            ∈ run-event-state(r;e2)))) supposing 
       ((run-event-step(e1) ≤ run-event-step(e2)) and 
       (run-event-loc(e1) = run-event-loc(e2) ∈ Id))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}n2m:\mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}l2m:Id  {}\mrightarrow{}  pMsg(P.M[P]).  \mforall{}S0:System(P.M[P]).  \mforall{}env:pEnvType(P.M[P]).
        let  r  =  pRun(S0;env;n2m;l2m)  in
                \mforall{}e1,e2:runEvents(r).
                    (\mforall{}P:Process(P.M[P])
                          ((P  \mmember{}  run-prior-state(S0;r;e1))
                          {}\mRightarrow{}  (iterate-Process(P;map(\mlambda{}e.run-event-msg(r;e);run-event-interval(r;e1;e2)))
                                    \mmember{}  run-event-state(r;e2))))  supposing 
                          ((run-event-step(e1)  \mleq{}  run-event-step(e2))  and 
                          (run-event-loc(e1)  =  run-event-loc(e2))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(InstLemma  `run-event-state-next`  []
  THEN  RepeatFor  6  ((ParallelLast'  THENA  Auto))
  THEN  MoveToConcl  (-1)
  THEN  GenConclAtAddr  [1;1]
  THEN  RenameVar  `r'  (-2)
  THEN  RepUR  ``let``  0
  THEN  (Assert  r  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  (D  0  THENA  Auto))

---

Home Index