---

Step * 1 1 1 2 2 1 2 of Lemma pRun-invariant3

.....wf..... 
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
11. t : ℤ@i
12. 0 < t@i
13. ∀e1,e2:runEvents(r).
      ((run-event-loc(e1) = run-event-loc(e2) ∈ Id)
      ⇒ 0 < run-event-step(e1)
      ⇒ (run-event-step(e1) ≤ run-event-step(e2))
      ⇒ run-event-step(e2) < t - 1
      ⇒ (∀P:Process(P.M[P])
            ((P ∈ run-event-state-when(r;e1))
            ⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2))) ∈ run-event-state(r;e2)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. 0 < run-event-step(e1)@i
18. run-event-step(e1) ≤ run-event-step(e2)@i
19. run-event-step(e2) < t@i
20. P : Process(P.M[P])@i
21. (P ∈ run-event-state-when(r;e1))@i
22. run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List)
23. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
24. runEvents(pRun(S0;env;n2m;l2m)) = runEvents(r) ∈ Type
25. ∀r:fulpRunType(P.M[P]). ∀e1,e2:runEvents(r).
      (map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)) ∈ pMsg(P.M[P]) List)
26. ∀e:runEvents(pRun(S0;env;n2m;l2m))
      (run-event-state(pRun(S0;env;n2m;l2m);e)
      = rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e))));
                run-event-state-when(pRun(S0;env;n2m;l2m);e)))
      ∈ (Process(P.M[P]) List))
27. run-event-state(pRun(S0;env;n2m;l2m);e2)
= rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e2))));
          run-event-state-when(pRun(S0;env;n2m;l2m);e2)))
∈ (Process(P.M[P]) List)
28. z : fulpRunType(P.M[P])
29. z = pRun(S0;env;n2m;l2m) ∈ fulpRunType(P.M[P])
⊢ (iterate-Process(P;map(λe.run-event-msg(z;e);run-event-interval(z;e1;e2))) ∈ run-event-state(z;e2)) ∈ ℙ
BY
{ ((Assert runEvents(pRun(S0;env;n2m;l2m)) ⊆r runEvents(z) BY
          (At Type ((HypSubst (-1) 0 THEN Auto))⋅ THEN UsingVars [`M'] (BLemma `runEvents_wf`) THEN Auto))
   THEN MemCD
   ) }

1
.....subterm..... T:t
3:n
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
11. t : ℤ@i
12. 0 < t@i
13. ∀e1,e2:runEvents(r).
      ((run-event-loc(e1) = run-event-loc(e2) ∈ Id)
      ⇒ 0 < run-event-step(e1)
      ⇒ (run-event-step(e1) ≤ run-event-step(e2))
      ⇒ run-event-step(e2) < t - 1
      ⇒ (∀P:Process(P.M[P])
            ((P ∈ run-event-state-when(r;e1))
            ⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2))) ∈ run-event-state(r;e2)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. 0 < run-event-step(e1)@i
18. run-event-step(e1) ≤ run-event-step(e2)@i
19. run-event-step(e2) < t@i
20. P : Process(P.M[P])@i
21. (P ∈ run-event-state-when(r;e1))@i
22. run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List)
23. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
24. runEvents(pRun(S0;env;n2m;l2m)) = runEvents(r) ∈ Type
25. ∀r:fulpRunType(P.M[P]). ∀e1,e2:runEvents(r).
      (map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)) ∈ pMsg(P.M[P]) List)
26. ∀e:runEvents(pRun(S0;env;n2m;l2m))
      (run-event-state(pRun(S0;env;n2m;l2m);e)
      = rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e))));
                run-event-state-when(pRun(S0;env;n2m;l2m);e)))
      ∈ (Process(P.M[P]) List))
27. run-event-state(pRun(S0;env;n2m;l2m);e2)
= rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e2))));
          run-event-state-when(pRun(S0;env;n2m;l2m);e2)))
∈ (Process(P.M[P]) List)
28. z : fulpRunType(P.M[P])
29. z = pRun(S0;env;n2m;l2m) ∈ fulpRunType(P.M[P])
30. runEvents(pRun(S0;env;n2m;l2m)) ⊆r runEvents(z)
⊢ Process(P.M[P]) ∈ Type

2
.....subterm..... T:t
1:n
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
11. t : ℤ@i
12. 0 < t@i
13. ∀e1,e2:runEvents(r).
      ((run-event-loc(e1) = run-event-loc(e2) ∈ Id)
      ⇒ 0 < run-event-step(e1)
      ⇒ (run-event-step(e1) ≤ run-event-step(e2))
      ⇒ run-event-step(e2) < t - 1
      ⇒ (∀P:Process(P.M[P])
            ((P ∈ run-event-state-when(r;e1))
            ⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2))) ∈ run-event-state(r;e2)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. 0 < run-event-step(e1)@i
18. run-event-step(e1) ≤ run-event-step(e2)@i
19. run-event-step(e2) < t@i
20. P : Process(P.M[P])@i
21. (P ∈ run-event-state-when(r;e1))@i
22. run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List)
23. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
24. runEvents(pRun(S0;env;n2m;l2m)) = runEvents(r) ∈ Type
25. ∀r:fulpRunType(P.M[P]). ∀e1,e2:runEvents(r).
      (map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)) ∈ pMsg(P.M[P]) List)
26. ∀e:runEvents(pRun(S0;env;n2m;l2m))
      (run-event-state(pRun(S0;env;n2m;l2m);e)
      = rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e))));
                run-event-state-when(pRun(S0;env;n2m;l2m);e)))
      ∈ (Process(P.M[P]) List))
27. run-event-state(pRun(S0;env;n2m;l2m);e2)
= rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e2))));
          run-event-state-when(pRun(S0;env;n2m;l2m);e2)))
∈ (Process(P.M[P]) List)
28. z : fulpRunType(P.M[P])
29. z = pRun(S0;env;n2m;l2m) ∈ fulpRunType(P.M[P])
30. runEvents(pRun(S0;env;n2m;l2m)) ⊆r runEvents(z)
⊢ iterate-Process(P;map(λe.run-event-msg(z;e);run-event-interval(z;e1;e2))) ∈ Process(P.M[P])

3
.....subterm..... T:t
2:n
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
11. t : ℤ@i
12. 0 < t@i
13. ∀e1,e2:runEvents(r).
      ((run-event-loc(e1) = run-event-loc(e2) ∈ Id)
      ⇒ 0 < run-event-step(e1)
      ⇒ (run-event-step(e1) ≤ run-event-step(e2))
      ⇒ run-event-step(e2) < t - 1
      ⇒ (∀P:Process(P.M[P])
            ((P ∈ run-event-state-when(r;e1))
            ⇒ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2))) ∈ run-event-state(r;e2)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. 0 < run-event-step(e1)@i
18. run-event-step(e1) ≤ run-event-step(e2)@i
19. run-event-step(e2) < t@i
20. P : Process(P.M[P])@i
21. (P ∈ run-event-state-when(r;e1))@i
22. run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List)
23. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
24. runEvents(pRun(S0;env;n2m;l2m)) = runEvents(r) ∈ Type
25. ∀r:fulpRunType(P.M[P]). ∀e1,e2:runEvents(r).
      (map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)) ∈ pMsg(P.M[P]) List)
26. ∀e:runEvents(pRun(S0;env;n2m;l2m))
      (run-event-state(pRun(S0;env;n2m;l2m);e)
      = rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e))));
                run-event-state-when(pRun(S0;env;n2m;l2m);e)))
      ∈ (Process(P.M[P]) List))
27. run-event-state(pRun(S0;env;n2m;l2m);e2)
= rev(map(λP.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e2))));
          run-event-state-when(pRun(S0;env;n2m;l2m);e2)))
∈ (Process(P.M[P]) List)
28. z : fulpRunType(P.M[P])
29. z = pRun(S0;env;n2m;l2m) ∈ fulpRunType(P.M[P])
30. runEvents(pRun(S0;env;n2m;l2m)) ⊆r runEvents(z)
⊢ run-event-state(z;e2) ∈ Process(P.M[P]) List

---

Latex:

---

Latex:
.....wf..... 
1.  M  :  Type  {}\mrightarrow{}  Type
2.  Continuous+(P.M[P])
3.  n2m  :  \mBbbN{}  {}\mrightarrow{}  pMsg(P.M[P])@i
4.  l2m  :  Id  {}\mrightarrow{}  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@i
9.  r  \mmember{}  pRunType(P.M[P])
10.  \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))@i
11.  t  :  \mBbbZ{}@i
12.  0  <  t@i
13.  \mforall{}e1,e2:runEvents(r).
            ((run-event-loc(e1)  =  run-event-loc(e2))
            {}\mRightarrow{}  0  <  run-event-step(e1)
            {}\mRightarrow{}  (run-event-step(e1)  \mleq{}  run-event-step(e2))
            {}\mRightarrow{}  run-event-step(e2)  <  t  -  1
            {}\mRightarrow{}  (\mforall{}P:Process(P.M[P])
                        ((P  \mmember{}  run-event-state-when(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)))))@i
14.  e1  :  runEvents(r)@i
15.  e2  :  runEvents(r)@i
16.  run-event-loc(e1)  =  run-event-loc(e2)@i
17.  0  <  run-event-step(e1)@i
18.  run-event-step(e1)  \mleq{}  run-event-step(e2)@i
19.  run-event-step(e2)  <  t@i
20.  P  :  Process(P.M[P])@i
21.  (P  \mmember{}  run-event-state-when(r;e1))@i
22.  run-prior-state(S0;r;e2)  =  run-prior-state(S0;r;e1)
23.  run-event-interval(r;e1;e2)  =  [e2]
24.  runEvents(pRun(S0;env;n2m;l2m))  =  runEvents(r)
25.  \mforall{}r:fulpRunType(P.M[P]).  \mforall{}e1,e2:runEvents(r).
            (map(\mlambda{}e.run-event-msg(r;e);run-event-interval(r;e1;e2))  \mmember{}  pMsg(P.M[P])  List)
26.  \mforall{}e:runEvents(pRun(S0;env;n2m;l2m))
            (run-event-state(pRun(S0;env;n2m;l2m);e)
            =  rev(map(\mlambda{}P.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e))));
                                run-event-state-when(pRun(S0;env;n2m;l2m);e))))
27.  run-event-state(pRun(S0;env;n2m;l2m);e2)
=  rev(map(\mlambda{}P.(fst(Process-apply(P;run-event-msg(pRun(S0;env;n2m;l2m);e2))));
                    run-event-state-when(pRun(S0;env;n2m;l2m);e2)))
28.  z  :  fulpRunType(P.M[P])
29.  z  =  pRun(S0;env;n2m;l2m)
\mvdash{}  (iterate-Process(P;map(\mlambda{}e.run-event-msg(z;e);run-event-interval(z;e1;e2)))
        \mmember{}  run-event-state(z;e2))  \mmember{}  \mBbbP{}


By

---

Latex:
((Assert  runEvents(pRun(S0;env;n2m;l2m))  \msubseteq{}r  runEvents(z)  BY
                (At  Type  ((HypSubst  (-1)  0  THEN  Auto))\mcdot{}
                  THEN  UsingVars  [`M']  (BLemma  `runEvents\_wf`)
                  THEN  Auto))
  THEN  MemCD
  )

---

Home Index