---

Step * of Lemma run-event-state-next2

∀[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)
          (run-event-state(r;e)
          = rev(map(λP.(fst(Process-apply(P;run-event-msg(r;e))));run-event-state-when(r;e)))
          ∈ (Process(P.M[P]) List)) 
  supposing Continuous+(P.M[P])
BY
{ (Auto
   THEN (Assert pRun(S0;env;n2m;l2m) ∈ pRunType(P.M[P]) BY
               (DoSubsume THEN Auto))
   THEN RepUR ``let`` 0
   THEN Auto
   THEN D -1
   THEN D -2
   THEN All Reduce
   THEN RenameVar `n' (-3)
   THEN RenameVar `x' (-2)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN Auto
   THEN RW (AddrC [2] 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-state-when 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
⊢ mapfilter(λc.(snd(c));λc.fst(c) = x;v7)
= rev(map(λP.(fst(Process-apply(P;x5)));let info,Cs,G = pRun(S0;env;n2m;l2m) (n - 1) in 
          mapfilter(λc.(snd(c));λc.fst(c) = x;Cs)))
∈ (Process(P.M[P]) List)

---

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)
                    (run-event-state(r;e)
                    =  rev(map(\mlambda{}P.(fst(Process-apply(P;run-event-msg(r;e))));run-event-state-when(r;e)))) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
(Auto
  THEN  (Assert  pRun(S0;env;n2m;l2m)  \mmember{}  pRunType(P.M[P])  BY
                          (DoSubsume  THEN  Auto))
  THEN  RepUR  ``let``  0
  THEN  Auto
  THEN  D  -1
  THEN  D  -2
  THEN  All  Reduce
  THEN  RenameVar  `n'  (-3)
  THEN  RenameVar  `x'  (-2)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  Auto
  THEN  RW  (AddrC  [2]  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
                          \mcdot{}
                          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-state-when  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