---

Step * 1 3 3 1 1 1 1 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
6. C3 : Id@i
7. C4 : Process(P.M[P])@i
8. C1 : component(P.M[P]) List@i
9. C5 : Id@i
10. C6 : Process(P.M[P])@i
11. C2 : component(P.M[P]) List@i
12. ||[<C3, C4> / C1]|| = ||[<C5, C6> / C2]|| ∈ ℤ@i
13. ∀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
14. ∀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]))))))
15. S3 : component(P.M[P]) List@i
16. S4 : LabeledDAG(pInTransit(P.M[P]))@i
17. S5 : component(P.M[P]) List@i
18. S6 : LabeledDAG(pInTransit(P.M[P]))@i
19. system-equiv(P.M[P];<S3, S4>;<S5, S6>) ∧ (<S3, S4> = <S5, S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))@i
20. C3 = C5 ∈ Id
21. C4
    ≡
    C6
22. C5 = x ∈ Id
⊢ system-equiv(P.M[P];let Q,ext = Process-apply(C4;m) 
                      in <[<C5, Q> / S3], lg-append(S4;add-cause(<t, x>;ext))>;let Q,ext = Process-apply(C6;m) 
                                                        in <[<C5, Q> / S5], lg-append(S6;add-cause(<t, x>;ext))>)
BY
{ (Unfold `process-equiv` (-2)
   THEN (InstHyp [⌜[m]⌝] (-2)⋅ THENA Auto)
   THEN RepUR ``Process-stream`` -1
   THEN (RWO "data-stream-cons" (-1) THENA Auto)
   THEN Reduce (-1)
   THEN Unfold `dataflow-ap` -1
   THEN Fold `Process-apply` (-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. C3 : Id@i
7. C4 : Process(P.M[P])@i
8. C1 : component(P.M[P]) List@i
9. C5 : Id@i
10. C6 : Process(P.M[P])@i
11. C2 : component(P.M[P]) List@i
12. ||[<C3, C4> / C1]|| = ||[<C5, C6> / C2]|| ∈ ℤ@i
13. ∀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
14. ∀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]))))))
15. S3 : component(P.M[P]) List@i
16. S4 : LabeledDAG(pInTransit(P.M[P]))@i
17. S5 : component(P.M[P]) List@i
18. S6 : LabeledDAG(pInTransit(P.M[P]))@i
19. system-equiv(P.M[P];<S3, S4>;<S5, S6>) ∧ (<S3, S4> = <S5, S6> ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))@i
20. C3 = C5 ∈ Id
21. ∀msgs:pMsg(P.M[P]) List. (Process-stream(C4;msgs) = Process-stream(C6;msgs) ∈ (pExt(P.M[P]) List))
22. C5 = x ∈ Id
23. [snd(Process-apply(C4;m))] = [snd(Process-apply(C6;m))] ∈ (pExt(P.M[P]) List)
⊢ system-equiv(P.M[P];let Q,ext = Process-apply(C4;m) 
                      in <[<C5, Q> / S3], lg-append(S4;add-cause(<t, x>;ext))>;let Q,ext = Process-apply(C6;m) 
                                                        in <[<C5, Q> / S5], lg-append(S6;add-cause(<t, x>;ext))>)

---

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.  C6  :  Process(P.M[P])@i
11.  C2  :  component(P.M[P])  List@i
12.  ||[<C3,  C4>  /  C1]||  =  ||[<C5,  C6>  /  C2]||@i
13.  \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
14.  \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))))
15.  S3  :  component(P.M[P])  List@i
16.  S4  :  LabeledDAG(pInTransit(P.M[P]))@i
17.  S5  :  component(P.M[P])  List@i
18.  S6  :  LabeledDAG(pInTransit(P.M[P]))@i
19.  system-equiv(P.M[P];<S3,  S4><S5,  S6>)  \mwedge{}  (<S3,  S4>  =  <S5,  S6>)@i
20.  C3  =  C5
21.  C4
        \mequiv{}
        C6
22.  C5  =  x
\mvdash{}  system-equiv(P.M[P];let  Q,ext  =  Process-apply(C4;m) 
                                            in  <[<C5,  Q>  /  S3],  lg-append(S4;add-cause(<t,  x>ext))>let  Q,ext  =  Process-a\000Cpply(C6;m) 
                                                                                                                in  <[<C5,  Q>  /  S5]
                                                                                                                      ,  lg-append(S6;add-cause(<t,  x>ext))
                                                                                                                      >)


By

---

Latex:
(Unfold  `process-equiv`  (-2)
  THEN  (InstHyp  [\mkleeneopen{}[m]\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  RepUR  ``Process-stream``  -1
  THEN  (RWO  "data-stream-cons"  (-1)  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  Unfold  `dataflow-ap`  -1
  THEN  Fold  `Process-apply`  (-1))

---

Home Index