Step
*
1
1
2
of Lemma
pRun-invariant3
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))
BY
{ OnMaybeHyp 10 (\h. ((InstHyp [⌈e2⌉] h⋅ THENA Complete (Auto))
THEN ((FLemma `sub-mset-contains` [-1] THENA CompleteAuto)
THEN Unfold `l_contains` (-1)
THEN (RWO "l_all_iff" (-1) THENA Auto)
THEN (BHyp (-1) THENA CompleteAuto))
THEN (RepeatFor 2 (Thin (-1))
THEN HypSubst' (-1) 0⋅
THEN RepUR ``iterate-Process`` 0⋅
THEN ((RWW "map_append_sq iterate-dataflow-append" 0⋅ THENM Reduce 0) THENA Auto)
THEN Fold `iterate-Process` 0
THEN (Unfold `dataflow-ap` 0
THEN Fold `Process-apply` 0
THEN ((BLemma `member_map` THENM Reduce 0)
THEN Auto
THEN With ⌈iterate-Process(P;map(λe.run-event-msg(r;e);
run-event-interval(r;e1;e)))⌉ (D 0)⋅
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. 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;e))) ∈ 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{} 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. e : runEvents(r)
23. run-event-step(e) < run-event-step(e2)
24. run-event-step(e1) \mleq{} run-event-step(e)
25. run-event-loc(e1) = run-event-loc(e)
26. run-prior-state(S0;r;e2) = run-event-state(r;e)
27. run-event-interval(r;e1;e2) = (run-event-interval(r;e1;e) @ [e2])
\mvdash{} (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:
OnMaybeHyp 10 (\mbackslash{}h. ((InstHyp [\mkleeneopen{}e2\mkleeneclose{}] h\mcdot{} THENA Complete (Auto))
THEN ((FLemma `sub-mset-contains` [-1] THENA CompleteAuto)
THEN Unfold `l\_contains` (-1)
THEN (RWO "l\_all\_iff" (-1) THENA Auto)
THEN (BHyp (-1) THENA CompleteAuto))
THEN (RepeatFor 2 (Thin (-1))
THEN HypSubst' (-1) 0\mcdot{}
THEN RepUR ``iterate-Process`` 0\mcdot{}
THEN ((RWW "map\_append\_sq iterate-dataflow-append" 0\mcdot{} THENM Reduce 0)
THENA Auto
)
THEN Fold `iterate-Process` 0
THEN (Unfold `dataflow-ap` 0
THEN Fold `Process-apply` 0
THEN ((BLemma `member\_map` THENM Reduce 0)
THEN Auto
THEN With \mkleeneopen{}iterate-Process(P;map(\mlambda{}e.run-event-msg(r;e);
run-event-interval(r;e1;e)))\mkleeneclose{}
(D 0)\mcdot{}
THEN Auto)\mcdot{})\mcdot{})\mcdot{}))\mcdot{}
Home
Index