---

Step * of Lemma deliver-msg_functionality

∀[M:Type ⟶ Type]
  ∀t:ℕ. ∀x:Id. ∀m:pMsg(P.M[P]). ∀G1,G2:LabeledDAG(pInTransit(P.M[P])). ∀Cs1,Cs2:component(P.M[P]) List.
    ((∀k:ℕ||Cs1||. let x,P = Cs1[k] in let z,Q = Cs2[k] in (x = z ∈ Id) ∧ P≡Q)
       ⇒ (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
          ∧ (deliver-msg(t;m;x;Cs1;G1)
            = deliver-msg(t;m;x;Cs2;G2)
            ∈ (Top × LabeledDAG(pInTransit(P.M[P])))))) supposing 
       ((||Cs1|| = ||Cs2|| ∈ ℤ) and 
       (G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P])))) 
  supposing Continuous+(P.M[P])
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `deliver-msg` 0
   THEN (Assert system-equiv(P.M[P];<[], G1>;<[], G2>) ∧ (<[], G1> = <[], G2> ∈ (Top × LabeledDAG(pInTransit(P.M[P])))) \000CBY
               (Unfold `system-equiv` 0 THEN RW (AddrC [1] (TagC (mk_tag_term 2))) 0 THEN Reduce 0 THEN Auto))⋅
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜<[], G1> = S1 ∈ System(P.M[P])⌝⋅ THENA Auto)
   THEN (GenConcl ⌜<[], G2> = S2 ∈ System(P.M[P])⌝⋅ THENA Auto)
   THEN ThinVar `G1'
   THEN ThinVar `G2'
   THEN RepeatFor 6 (MoveToConcl (-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
⊢ ∀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]))))))))

---

Latex:

---

Latex:
\mforall{}[M:Type  {}\mrightarrow{}  Type]
    \mforall{}t:\mBbbN{}.  \mforall{}x:Id.  \mforall{}m:pMsg(P.M[P]).  \mforall{}G1,G2:LabeledDAG(pInTransit(P.M[P])).
    \mforall{}Cs1,Cs2:component(P.M[P])  List.
        ((\mforall{}k:\mBbbN{}||Cs1||.  let  x,P  =  Cs1[k]  in  let  z,Q  =  Cs2[k]  in  (x  =  z)  \mwedge{}  P\mequiv{}Q)
              {}\mRightarrow{}  (system-equiv(P.M[P];deliver-msg(t;m;x;Cs1;G1);deliver-msg(t;m;x;Cs2;G2))
                    \mwedge{}  (deliver-msg(t;m;x;Cs1;G1)  =  deliver-msg(t;m;x;Cs2;G2))))  supposing 
              ((||Cs1||  =  ||Cs2||)  and 
              (G1  =  G2)) 
    supposing  Continuous+(P.M[P])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `deliver-msg`  0
  THEN  (Assert  system-equiv(P.M[P];<[],  G1><[],  G2>)  \mwedge{}  (<[],  G1>  =  <[],  G2>)  BY
                          (Unfold  `system-equiv`  0
                            THEN  RW  (AddrC  [1]  (TagC  (mk\_tag\_term  2)))  0
                            THEN  Reduce  0
                            THEN  Auto))\mcdot{}
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}<[],  G1>  =  S1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}<[],  G2>  =  S2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `G1'
  THEN  ThinVar  `G2'
  THEN  RepeatFor  6  (MoveToConcl  (-1)))

---

Home Index