Step
*
1
3
3
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]) List
((||C1|| = ||Cs2|| ∈ ℤ)
⇒ (∀k:ℕ||C1||. let x,P = C1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
⇒ (∀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:
Cs2
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:
Cs2
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))))))@i
9. Cs2 : component(P.M[P])@i
10. C2 : component(P.M[P]) List@i
11. (||[Cs1 / C1]|| = ||C2|| ∈ ℤ)
⇒ (∀k:ℕ||[Cs1 / C1]||. let x,P = [Cs1 / C1][k] in let z,Q = C2[k] in (x = z ∈ Id) ∧ P≡Q)
⇒ (∀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:
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:
C2
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))))))@i
⊢ (||[Cs1 / C1]|| = ||[Cs2 / C2]|| ∈ ℤ)
⇒ (∀k:ℕ||[Cs1 / C1]||. let x,P = [Cs1 / C1][k] in let z,Q = [Cs2 / C2][k] in (x = z ∈ Id) ∧ P≡Q)
⇒ (∀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
{ ((D 0 THENA Auto)
THEN Thin (-2)
THEN (D 0 THENA (Auto THEN Auto'))
THEN ((InstHyp [⌜C2⌝] (-5)⋅
THENA (Auto'
THEN InstHyp [⌜k + 1⌝] (-2)⋅
THEN Auto'
THEN RWO "select_cons_tl" (-1)
THEN Auto
THEN NthHypSq (-1)
THEN EqCD
THEN Auto)
)
THEN Thin (-6)
)⋅) }
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. 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]))))))
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. \mforall{}Cs2:component(P.M[P]) List
((||C1|| = ||Cs2||)
{}\mRightarrow{} (\mforall{}k:\mBbbN{}||C1||. let x,P = C1[k] in let z,Q = Cs2[k] in (x = z) \mwedge{} P\mequiv{}Q)
{}\mRightarrow{} (\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:
Cs2
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:
Cs2
with starting value:
S2))))))@i
9. Cs2 : component(P.M[P])@i
10. C2 : component(P.M[P]) List@i
11. (||[Cs1 / C1]|| = ||C2||)
{}\mRightarrow{} (\mforall{}k:\mBbbN{}||[Cs1 / C1]||. let x,P = [Cs1 / C1][k] in let z,Q = C2[k] in (x = z) \mwedge{} P\mequiv{}Q)
{}\mRightarrow{} (\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:
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:
C2
with starting value:
S2)))))@i
\mvdash{} (||[Cs1 / C1]|| = ||[Cs2 / C2]||)
{}\mRightarrow{} (\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)
{}\mRightarrow{} (\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:
((D 0 THENA Auto)
THEN Thin (-2)
THEN (D 0 THENA (Auto THEN Auto'))
THEN ((InstHyp [\mkleeneopen{}C2\mkleeneclose{}] (-5)\mcdot{}
THENA (Auto'
THEN InstHyp [\mkleeneopen{}k + 1\mkleeneclose{}] (-2)\mcdot{}
THEN Auto'
THEN RWO "select\_cons\_tl" (-1)
THEN Auto
THEN NthHypSq (-1)
THEN EqCD
THEN Auto)
)
THEN Thin (-6)
)\mcdot{})
Home
Index