Step
*
1
3
3
1
1
1
of Lemma
deliver-msg_functionality
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. t : ℕ@i
4. x : Id@i
5. m : pMsg(P.M[P])@i
6. Cs1 : component(P.M[P])@i
7. C1 : component(P.M[P]) List@i
8. Cs2 : component(P.M[P])@i
9. C2 : component(P.M[P]) List@i
10. ||[Cs1 / C1]|| = ||[Cs2 / C2]|| ∈ ℤ@i
11. ∀k:ℕ||[Cs1 / C1]||. let x,P = [Cs1 / C1][k] in let z,Q = [Cs2 / C2][k] in (x = z ∈ Id) ∧ P≡Q@i
12. ∀S1,S2:System(P.M[P]).
((system-equiv(P.M[P];S1;S2) ∧ (S1 = S2 ∈ (Top × LabeledDAG(pInTransit(P.M[P])))))
⇒ (system-equiv(P.M[P];accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1);accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2))
∧ (accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1)
= accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))))
13. S1 : System(P.M[P])@i
14. S2 : System(P.M[P])@i
15. system-equiv(P.M[P];S1;S2) ∧ (S1 = S2 ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))@i
16. let x,P = Cs1
in let z,Q = Cs2
in (x = z ∈ Id) ∧ P≡Q
⊢ system-equiv(P.M[P];deliver-msg-to-comp(t;m;x;S1;Cs1);deliver-msg-to-comp(t;m;x;S2;Cs2))
∧ (deliver-msg-to-comp(t;m;x;S1;Cs1) = deliver-msg-to-comp(t;m;x;S2;Cs2) ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))
BY
{ (Reduce (-1)
THEN DVar `S1'
THEN DVar `S2'
THEN DVar `Cs1'
THEN DVar `Cs2'
THEN Reduce (-1)
THEN RepUR ``deliver-msg-to-comp`` 0
THEN (D -1 THEN HypSubst' (-2) 0 THEN AutoSplit)⋅) }
1
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. t : ℕ@i
4. x : Id@i
5. m : pMsg(P.M[P])@i
6. C3 : Id@i
7. C4 : Process(P.M[P])@i
8. C1 : component(P.M[P]) List@i
9. C5 : Id@i
10. C6 : Process(P.M[P])@i
11. C2 : component(P.M[P]) List@i
12. ||[<C3, C4> / C1]|| = ||[<C5, C6> / C2]|| ∈ ℤ@i
13. ∀k:ℕ||[<C3, C4> / C1]||. let x,P = [<C3, C4> / C1][k] in let z,Q = [<C5, C6> / C2][k] in (x = z ∈ Id) ∧ P≡Q@i
14. ∀S1,S2:System(P.M[P]).
((system-equiv(P.M[P];S1;S2) ∧ (S1 = S2 ∈ (Top × LabeledDAG(pInTransit(P.M[P])))))
⇒ (system-equiv(P.M[P];accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1);accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2))
∧ (accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1)
= accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))))
15. S3 : component(P.M[P]) List@i
16. S4 : LabeledDAG(pInTransit(P.M[P]))@i
17. S5 : component(P.M[P]) List@i
18. S6 : LabeledDAG(pInTransit(P.M[P]))@i
19. system-equiv(P.M[P];<S3, S4>;<S5, S6>) ∧ (<S3, S4> = <S5, S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))@i
20. C3 = C5 ∈ Id
21. C4
≡
C6
22. C5 = x ∈ Id
⊢ system-equiv(P.M[P];let Q,ext = Process-apply(C4;m)
in <[<C5, Q> / S3], lg-append(S4;add-cause(<t, x>;ext))>;let Q,ext = Process-apply(C6;m)
in <[<C5, Q> / S5], lg-append(S6;add-cause(<t, x>;ext))>)
∧ (let Q,ext = Process-apply(C4;m)
in <[<C5, Q> / S3], lg-append(S4;add-cause(<t, x>;ext))>
= let Q,ext = Process-apply(C6;m)
in <[<C5, Q> / S5], lg-append(S6;add-cause(<t, x>;ext))>
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))
2
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. t : ℕ@i
4. x : Id@i
5. m : pMsg(P.M[P])@i
6. C3 : Id@i
7. C4 : Process(P.M[P])@i
8. C1 : component(P.M[P]) List@i
9. C5 : Id@i
10. ¬(C5 = x ∈ Id)
11. C6 : Process(P.M[P])@i
12. C2 : component(P.M[P]) List@i
13. ||[<C3, C4> / C1]|| = ||[<C5, C6> / C2]|| ∈ ℤ@i
14. ∀k:ℕ||[<C3, C4> / C1]||. let x,P = [<C3, C4> / C1][k] in let z,Q = [<C5, C6> / C2][k] in (x = z ∈ Id) ∧ P≡Q@i
15. ∀S1,S2:System(P.M[P]).
((system-equiv(P.M[P];S1;S2) ∧ (S1 = S2 ∈ (Top × LabeledDAG(pInTransit(P.M[P])))))
⇒ (system-equiv(P.M[P];accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1);accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2))
∧ (accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1)
= accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))))
16. S3 : component(P.M[P]) List@i
17. S4 : LabeledDAG(pInTransit(P.M[P]))@i
18. S5 : component(P.M[P]) List@i
19. S6 : LabeledDAG(pInTransit(P.M[P]))@i
20. system-equiv(P.M[P];<S3, S4>;<S5, S6>) ∧ (<S3, S4> = <S5, S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))@i
21. C3 = C5 ∈ Id
22. C4
≡
C6
⊢ system-equiv(P.M[P];<[<C5, C4> / S3], S4>;<[<C5, C6> / S5], S6>)
∧ (<[<C5, C4> / S3], S4> = <[<C5, C6> / S5], S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))
Latex:
Latex:
1. [M] : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. t : \mBbbN{}@i
4. x : Id@i
5. m : pMsg(P.M[P])@i
6. Cs1 : component(P.M[P])@i
7. C1 : component(P.M[P]) List@i
8. Cs2 : component(P.M[P])@i
9. C2 : component(P.M[P]) List@i
10. ||[Cs1 / C1]|| = ||[Cs2 / C2]||@i
11. \mforall{}k:\mBbbN{}||[Cs1 / C1]||. let x,P = [Cs1 / C1][k] in let z,Q = [Cs2 / C2][k] in (x = z) \mwedge{} P\mequiv{}Q@i
12. \mforall{}S1,S2:System(P.M[P]).
((system-equiv(P.M[P];S1;S2) \mwedge{} (S1 = S2))
{}\mRightarrow{} (system-equiv(P.M[P];accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1);accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2))
\mwedge{} (accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C1
with starting value:
S1)
= accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
C2
with starting value:
S2))))
13. S1 : System(P.M[P])@i
14. S2 : System(P.M[P])@i
15. system-equiv(P.M[P];S1;S2) \mwedge{} (S1 = S2)@i
16. let x,P = Cs1
in let z,Q = Cs2
in (x = z) \mwedge{} P\mequiv{}Q
\mvdash{} system-equiv(P.M[P];deliver-msg-to-comp(t;m;x;S1;Cs1);deliver-msg-to-comp(t;m;x;S2;Cs2))
\mwedge{} (deliver-msg-to-comp(t;m;x;S1;Cs1) = deliver-msg-to-comp(t;m;x;S2;Cs2))
By
Latex:
(Reduce (-1)
THEN DVar `S1'
THEN DVar `S2'
THEN DVar `Cs1'
THEN DVar `Cs2'
THEN Reduce (-1)
THEN RepUR ``deliver-msg-to-comp`` 0
THEN (D -1 THEN HypSubst' (-2) 0 THEN AutoSplit)\mcdot{})
Home
Index