---

Step * 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
⊢ ∀Cs1,Cs2:component(P.M[P]) List.
    ((||Cs1|| = ||Cs2|| ∈ ℤ)
    ⇒ (∀k:ℕ||Cs1||. let x,P = Cs1[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
                                  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
                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
⊢ λCs1.∀Cs2:component(P.M[P]) List
         ((||Cs1|| = ||Cs2|| ∈ ℤ)
         ⇒ (∀k:ℕ||Cs1||. let x,P = Cs1[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
                                       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
                     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
⊢ ∀Cs2:component(P.M[P]) List
    ((||[]|| = ||Cs2|| ∈ ℤ)
    ⇒ (∀k:ℕ||[]||. let x,P = [][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:
                                    []
                                  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:
                  []
                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]))))))))

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
⊢ ∀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]))))))))

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
⊢ ∀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])))))))) ∈ ℙ

---

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
\mvdash{}  \mforall{}Cs1,Cs2:component(P.M[P])  List.
        ((||Cs1||  =  ||Cs2||)
        {}\mRightarrow{}  (\mforall{}k:\mBbbN{}||Cs1||.  let  x,P  =  Cs1[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
                                                                    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
                                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