---

Step * 1 3 4 of Lemma deliver-msg_functionality

.....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]))))))) ∈ ℙ
BY
{ ((RepeatFor 5 (MemCD) THEN Try (CompleteAuto))
   THEN (GenConclAtAddrType  ⌈System(P.M[P])⌉ [2;2;2]⋅ THENA Auto)
   THEN (GenConclAtAddrType  ⌈System(P.M[P])⌉ [2;2;3]⋅ THENA Auto)
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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
\mvdash{}  (||[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)))))  \mmember{}  \mBbbP{}


By

---

Latex:
((RepeatFor  5  (MemCD)  THEN  Try  (CompleteAuto))
  THEN  (GenConclAtAddrType    \mkleeneopen{}System(P.M[P])\mkleeneclose{}  [2;2;2]\mcdot{}  THENA  Auto)
  THEN  (GenConclAtAddrType    \mkleeneopen{}System(P.M[P])\mkleeneclose{}  [2;2;3]\mcdot{}  THENA  Auto)
  THEN  Auto)

---

Home Index