Step
*
1
1
1
of Lemma
pRun-invariant2
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)
⇒ (run-event-step(e1) ≤ run-event-step(e2))
⇒ run-event-step(e2) < t - 1
⇒ (∀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)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. run-event-step(e1) ≤ run-event-step(e2)@i
18. run-event-step(e2) < t@i
19. P : Process(P.M[P])@i
20. (P ∈ run-prior-state(S0;r;e1))@i
⊢ (iterate-Process(P;map(λe.run-event-msg(r;e);run-event-interval(r;e1;e2)))
∈ map(λP.(fst(Process-apply(P;run-event-msg(r;e2))));run-prior-state(S0;r;e2)))
BY
{ ((InstLemma `run-event-interval-cases` [⌈M⌉;⌈S0⌉;⌈r⌉;⌈e1⌉;⌈e2⌉]⋅ THENA Auto)
THEN D (-1)
THEN ExRepD
THEN HypSubst' (-1) 0) }
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)
⇒ (run-event-step(e1) ≤ run-event-step(e2))
⇒ run-event-step(e2) < t - 1
⇒ (∀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)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. run-event-step(e1) ≤ run-event-step(e2)@i
18. run-event-step(e2) < t@i
19. P : Process(P.M[P])@i
20. (P ∈ run-prior-state(S0;r;e1))@i
21. run-prior-state(S0;r;e2) = run-prior-state(S0;r;e1) ∈ (Process(P.M[P]) List)
22. run-event-interval(r;e1;e2) = [e2] ∈ (runEvents(r) List)
⊢ (iterate-Process(P;map(λe.run-event-msg(r;e);[e2]))
∈ map(λP.(fst(Process-apply(P;run-event-msg(r;e2))));run-prior-state(S0;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)
⇒ (run-event-step(e1) ≤ run-event-step(e2))
⇒ run-event-step(e2) < t - 1
⇒ (∀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)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2) ∈ Id@i
17. run-event-step(e1) ≤ run-event-step(e2)@i
18. run-event-step(e2) < t@i
19. P : Process(P.M[P])@i
20. (P ∈ run-prior-state(S0;r;e1))@i
21. e : runEvents(r)
22. run-event-step(e) < run-event-step(e2)
23. run-event-step(e1) ≤ run-event-step(e)
24. run-event-loc(e1) = run-event-loc(e) ∈ Id
25. run-prior-state(S0;r;e2) = run-event-state(r;e) ∈ (Process(P.M[P]) List)
26. 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;e) @ [e2]))
∈ map(λP.(fst(Process-apply(P;run-event-msg(r;e2))));run-prior-state(S0;r;e2)))
Latex:
Latex:
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. \mbackslash{}\mbackslash{}\%5 : 0 < t@i
13. \mforall{}e1,e2:runEvents(r).
((run-event-loc(e1) = run-event-loc(e2))
{}\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-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)))))@i
14. e1 : runEvents(r)@i
15. e2 : runEvents(r)@i
16. run-event-loc(e1) = run-event-loc(e2)@i
17. run-event-step(e1) \mleq{} run-event-step(e2)@i
18. run-event-step(e2) < t@i
19. P : Process(P.M[P])@i
20. (P \mmember{} run-prior-state(S0;r;e1))@i
\mvdash{} (iterate-Process(P;map(\mlambda{}e.run-event-msg(r;e);run-event-interval(r;e1;e2)))
\mmember{} map(\mlambda{}P.(fst(Process-apply(P;run-event-msg(r;e2))));run-prior-state(S0;r;e2)))
By
Latex:
((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 HypSubst' (-1) 0)
Home
Index