Step
*
1
3
3
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]))))))
⊢ ∀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:
[Cs1 / C1]
with starting value:
S1);accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
[Cs2 / C2]
with starting value:
S2))
∧ (accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
[Cs1 / C1]
with starting value:
S1)
= accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
[Cs2 / C2]
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
THEN InstHyp [⌜deliver-msg-to-comp(t;m;x;S1;Cs1)⌝
;⌜deliver-msg-to-comp(t;m;x;S2;Cs2)⌝] (-4)⋅
THEN Try (Complete (Auto))) }
1
.....antecedent.....
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
⊢ 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]))))
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))))
\mvdash{} \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:
[Cs1 / C1]
with starting value:
S1);accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
[Cs2 / 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:
[Cs1 / C1]
with starting value:
S1)
= accumulate (with value S and list item C):
deliver-msg-to-comp(t;m;x;S;C)
over list:
[Cs2 / C2]
with starting value:
S2))))
By
Latex:
(RepeatFor 3 ((D 0 THENA Auto))
THEN InstHyp [\mkleeneopen{}deliver-msg-to-comp(t;m;x;S1;Cs1)\mkleeneclose{}
;\mkleeneopen{}deliver-msg-to-comp(t;m;x;S2;Cs2)\mkleeneclose{}] (-4)\mcdot{}
THEN Try (Complete (Auto)))
Home
Index