---

Step * of Lemma run-event-state-next

∀[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
        ∀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)) 
  supposing Continuous+(P.M[P])
BY
{ (Auto
   THEN (RepUR ``let`` 0 THEN (Assert pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P]) BY (DoSubsume THEN Auto)))
   THEN Auto⋅
   THEN D -1
   THEN D -2
   THEN All Reduce
   THEN (Assert ↑is-run-event(pRun(S0;env;n2m;l2m);e1;e2) BY
               (Unhide THEN Auto))
   THEN Thin (-2)
   THEN RenameVar `n' (-3)
   THEN RenameVar `x' (-2)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN Auto
   THEN RW (AddrC [3] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN MoveToConcl (-1)
   THEN (RepUR ``is-run-event run-event-msg run-info`` 0
         THEN Subst' pRun(S0;env;n2m;l2m) n ~ if (n =z 0)
         then <inr ⋅ , S0>
         else let n@0,m,nm = env n pRun(S0;env;n2m;l2m) in 
              do-chosen-command(n2m;l2m;n;snd((pRun(S0;env;n2m;l2m) (n - 1)));n@0;m;nm)
         fi  0
         THEN Try ((RW (AddrC [1;1] RecUnfoldTopAbC) 0 THEN Reduce 0 THEN Trivial))
         THEN AutoSplit
         THEN RepUR ``bfalse`` 0
         THEN Try (Complete (Auto))
         THEN ((GenConclAtAddr [1;1;1;1] THENA (Auto THEN DoSubsume THEN Auto THEN Auto))
               THEN RepeatFor 2 (D (-2))
               THEN Reduce 0
               THEN Thin 7
               THEN (GenConclAtAddr [1;1;1] THENA (Auto THEN DoSubsume THEN Auto THEN Auto))
               THEN (D (-2) THEN D -3)
               THEN Reduce 0
               THEN Try (Complete (Auto))
               THEN (D -2
                     THEN RepeatFor 2 (D (-4))
                     THEN Reduce 0
                     THEN RepUR ``run-event-local-pred run-event-history run-event-loc run-event-step let`` 0
                     THEN (D 0 THENA Auto)
                     THEN (RW assert_pushdownC (-1) THENA Auto)
                     THEN RevHypSubst' (-1) (-2)
                     THEN ThinVar `x4')⋅)⋅)⋅) }

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. n : {1...}
8. x : Id@i
9. v1 : ℕ@i
10. v3 : ℕ@i
11. v4 : Id@i
12. (env n pRun(S0;env;n2m;l2m)) = <v1, v3, v4> ∈ (ℕ × ℕ × Id)@i
13. x2 : ℤ × Id@i
14. x5 : pMsg(P.M[P])@i
15. v7 : component(P.M[P]) List@i
16. v8 : LabeledDAG(pInTransit(P.M[P]))@i
17. do-chosen-command(n2m;l2m;n;snd((pRun(S0;env;n2m;l2m) (n - 1)));v1;v3;v4)
= <inl <x2, x, x5>, v7, v8>
∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
⊢ sub-mset(Process(P.M[P]); map(λP.(fst(Process-apply(P;x5)));run-prior-state(S0;pRun(S0;env;n2m;l2m);<n, x>)); mapfilte\000Cr(λc.(snd(c));λc.fst(c) = x;v7))

---

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{}e:runEvents(r)
                    sub-mset(Process(P.M[P]);  map(\mlambda{}P.(fst(Process-apply(P;run-event-msg(r;e))));
                                                                                run-prior-state(S0;r;e));  run-event-state(r;e)) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(Auto
  THEN  (RepUR  ``let``  0
              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  All  Reduce
  THEN  (Assert  \muparrow{}is-run-event(pRun(S0;env;n2m;l2m);e1;e2)  BY
                          (Unhide  THEN  Auto))
  THEN  Thin  (-2)
  THEN  RenameVar  `n'  (-3)
  THEN  RenameVar  `x'  (-2)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  Auto
  THEN  RW  (AddrC  [3]  UnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  MoveToConcl  (-1)
  THEN 
  (RepUR  ``is-run-event  run-event-msg  run-info``  0
    THEN  Subst'  pRun(S0;env;n2m;l2m)  n  \msim{}  if  (n  =\msubz{}  0)
    then  <inr  \mcdot{}  ,  S0>
    else  let  n@0,m,nm  =  env  n  pRun(S0;env;n2m;l2m)  in 
              do-chosen-command(n2m;l2m;n;snd((pRun(S0;env;n2m;l2m)  (n  -  1)));n@0;m;nm)
    fi    0
    THEN  Try  ((RW  (AddrC  [1;1]  RecUnfoldTopAbC)  0  THEN  Reduce  0  THEN  Trivial))
    THEN  AutoSplit
    THEN  RepUR  ``bfalse``  0
    THEN  Try  (Complete  (Auto))
    THEN 
    ((GenConclAtAddr  [1;1;1;1]  THENA  (Auto  THEN  DoSubsume  THEN  Auto  THEN  Auto))
      THEN  RepeatFor  2  (D  (-2))
      THEN  Reduce  0
      THEN  Thin  7
      THEN  (GenConclAtAddr  [1;1;1]  THENA  (Auto  THEN  DoSubsume  THEN  Auto  THEN  Auto))
      THEN  (D  (-2)  THEN  D  -3)
      THEN  Reduce  0
      THEN  Try  (Complete  (Auto))
      THEN  (D  -2
                  THEN  RepeatFor  2  (D  (-4))
                  THEN  Reduce  0
                  THEN  RepUR  ``run-event-local-pred  run-event-history  run-event-loc  run-event-step  let``  0
                  THEN  (D  0  THENA  Auto)
                  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
                  THEN  RevHypSubst'  (-1)  (-2)
                  THEN  ThinVar  `x4')\mcdot{})\mcdot{})\mcdot{})

---

Home Index