Proof of Nuprl Lemma : deliver-msg

Step * 1 3 3 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))>)

∧ (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))>
  ∈ (Top × LabeledDAG(pInTransit(P.M[P]))))
BY
{ D 0 }

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

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))>)

2
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

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
⊢ 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))>
∈ (Top × LabeledDAG(pInTransit(P.M[P])))

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)) >) \mwedge{} (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 Latex: D 0 Home Index