Step
*
1
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
⊢ ∀Cs2:component(P.M[P]) List
((||[Cs1 / C1]|| = ||Cs2|| ∈ ℤ)
⇒ (∀k:ℕ||[Cs1 / C1]||. let x,P = [Cs1 / 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:
[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
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
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P]))))))))
BY
{ InductionOnListA }
1
.....wf.....
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
⊢ λCs2.((||[Cs1 / C1]|| = ||Cs2|| ∈ ℤ)
⇒ (∀k:ℕ||[Cs1 / C1]||. let x,P = [Cs1 / 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:
[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
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
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))))))) ∈ (component(P.M[P]) List) ─→ ℙ
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. 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
⊢ (||[Cs1 / C1]|| = ||[]|| ∈ ℤ)
⇒ (∀k:ℕ||[Cs1 / C1]||. let x,P = [Cs1 / C1][k] in let z,Q = [][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:
[]
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:
[]
with starting value:
S2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))))))
3
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])))))))
4
.....wf.....
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
⊢ (||[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]))))))) ∈ ℙ
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
\mvdash{} \mforall{}Cs2:component(P.M[P]) List
((||[Cs1 / C1]|| = ||Cs2||)
{}\mRightarrow{} (\mforall{}k:\mBbbN{}||[Cs1 / C1]||. let x,P = [Cs1 / 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:
[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
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
with starting value:
S2))))))
By
Latex:
InductionOnListA
Home
Index