---

Step * 1 3 3 1 1 of Lemma deliver-msg_functionality

.....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]))))
BY
{ ((InstHyp [⌜0⌝] 11⋅ THENA Auto') THEN Reduce (-1)) }

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]))))))
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
16. let x,P = Cs1 
    in let z,Q = Cs2 
       in (x = z ∈ Id) ∧ P≡Q
⊢ 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:
.....antecedent..... 
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))))
13.  S1  :  System(P.M[P])@i
14.  S2  :  System(P.M[P])@i
15.  system-equiv(P.M[P];S1;S2)  \mwedge{}  (S1  =  S2)@i
\mvdash{}  system-equiv(P.M[P];deliver-msg-to-comp(t;m;x;S1;Cs1);deliver-msg-to-comp(t;m;x;S2;Cs2))
\mwedge{}  (deliver-msg-to-comp(t;m;x;S1;Cs1)  =  deliver-msg-to-comp(t;m;x;S2;Cs2))


By

---

Latex:
((InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  11\mcdot{}  THENA  Auto')  THEN  Reduce  (-1))

---

Home Index