---

Step * 1 3 3 1 1 1 2 2 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. C3 : Id@i
7. C4 : Process(P.M[P])@i
8. C1 : component(P.M[P]) List@i
9. C5 : Id@i
10. ¬(C5 = x ∈ Id)
11. C6 : Process(P.M[P])@i
12. C2 : component(P.M[P]) List@i
13. ||[<C3, C4> / C1]|| = ||[<C5, C6> / C2]|| ∈ ℤ@i
14. ∀k:ℕ||[<C3, C4> / C1]||. let x,P = [<C3, C4> / C1][k] in let z,Q = [<C5, C6> / C2][k] in (x = z ∈ Id) ∧ P≡Q@i
15. ∀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]))))))
16. S3 : component(P.M[P]) List@i
17. S4 : LabeledDAG(pInTransit(P.M[P]))@i
18. S5 : component(P.M[P]) List@i
19. S6 : LabeledDAG(pInTransit(P.M[P]))@i
20. system-equiv(P.M[P];<S3, S4>;<S5, S6>) ∧ (<S3, S4> = <S5, S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))@i
21. C3 = C5 ∈ Id
22. C4
    ≡
    C6
⊢ <[<C5, C4> / S3], S4> = <[<C5, C6> / S5], S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P])))
BY
{ (EqCD THEN Auto)⋅ }

---

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.  C3  :  Id@i
7.  C4  :  Process(P.M[P])@i
8.  C1  :  component(P.M[P])  List@i
9.  C5  :  Id@i
10.  \mneg{}(C5  =  x)
11.  C6  :  Process(P.M[P])@i
12.  C2  :  component(P.M[P])  List@i
13.  ||[<C3,  C4>  /  C1]||  =  ||[<C5,  C6>  /  C2]||@i
14.  \mforall{}k:\mBbbN{}||[<C3,  C4>  /  C1]||
            let  x,P  =  [<C3,  C4>  /  C1][k] 
            in  let  z,Q  =  [<C5,  C6>  /  C2][k] 
                  in  (x  =  z)  \mwedge{}  P\mequiv{}Q@i
15.  \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))))
16.  S3  :  component(P.M[P])  List@i
17.  S4  :  LabeledDAG(pInTransit(P.M[P]))@i
18.  S5  :  component(P.M[P])  List@i
19.  S6  :  LabeledDAG(pInTransit(P.M[P]))@i
20.  system-equiv(P.M[P];<S3,  S4><S5,  S6>)  \mwedge{}  (<S3,  S4>  =  <S5,  S6>)@i
21.  C3  =  C5
22.  C4
        \mequiv{}
        C6
\mvdash{}  <[<C5,  C4>  /  S3],  S4>  =  <[<C5,  C6>  /  S5],  S6>


By

---

Latex:
(EqCD  THEN  Auto)\mcdot{}

---

Home Index