---

Step * 1 1 of Lemma pRun-invariant3

.....assertion..... 
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
⊢ ∀t:ℕ. ∀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
    ⇒ (∀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)))))
BY
{ (InductionOnNat
   THEN Auto'
   THEN ((InstLemma `run-event-interval-cases` [⌈M⌉;⌈S0⌉;⌈r⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
         THEN D (-1)
         THEN ExRepD
         THEN Try (Complete ((RepeatFor 2 (DVar `e1') THEN All (RepUR ``run-event-step``) THEN 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
11. t : ℤ@i
12. \\%5 : 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)
⊢ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2))) ∈ run-event-state(r;e2))

2
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. \\%5 : 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. e : runEvents(r)
23. run-event-step(e) < run-event-step(e2)
24. run-event-step(e1) ≤ run-event-step(e)
25. run-event-loc(e1) = run-event-loc(e) ∈ Id
26. run-prior-state(S0;r;e2) = run-event-state(r;e) ∈ (Process(P.M[P]) List)
27. run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2]) ∈ (runEvents(r) List)
⊢ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2))) ∈ run-event-state(r;e2))

---

Latex:

---

Latex:
.....assertion..... 
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
\mvdash{}  \mforall{}t:\mBbbN{}.  \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
        {}\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)))))


By

---

Latex:
(InductionOnNat
  THEN  Auto'
  THEN  ((InstLemma  `run-event-interval-cases`  [\mkleeneopen{}M\mkleeneclose{};\mkleeneopen{}S0\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  D  (-1)
              THEN  ExRepD
              THEN  Try  (Complete  ((RepeatFor  2  (DVar  `e1')  THEN  All  (RepUR  ``run-event-step``)  THEN  Auto)
                                                      \mcdot{})))\mcdot{})

---

Home Index