Step
*
1
2
2
1
1
1
1
1
of Lemma
pRun_functionality
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. (P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P])))
∧ (||P5|| = ||P7|| ∈ ℤ)
∧ (∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q)@i
17. m : ℕ@i
18. x : Id@i
19. G1 : LabeledDAG(pInTransit(P.M[P]))@i
20. G2 : LabeledDAG(pInTransit(P.M[P]))@i
21. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
22. L1 : pInTransit(P.M[P])@i
23. L2 : pInTransit(P.M[P])@i
24. L1 = L2 ∈ pInTransit(P.M[P])
⊢ system-equiv(P.M[P];snd(let ev,x@0,c = L1 in
if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P5;G1)>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P5;G1)>
if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P5;G1)>
if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P5;G1)>
else <inr ⋅ , P5, G1>
fi );snd(let ev,x@0,c = L2 in
if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P7;G2)>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P7;G2)>
if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P7;G2)>
if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P7;G2)>
else <inr ⋅ , P7, G2>
fi ))
∧ (let ev,x@0,c = L1 in
if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P5;G1)>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P5;G1)>
if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P5;G1)>
if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P5;G1)>
else <inr ⋅ , P5, G1>
fi
= let ev,x@0,c = L2 in
if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P7;G2)>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x@0;P7;G2)>
if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P7;G2)>
if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P7;G2)>
else <inr ⋅ , P7, G2>
fi
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
BY
{ (RepeatFor 2 (D (-3))
THEN (RepeatFor 2 (D (-2)) THEN Reduce 0)
THEN RepUR ``pInTransit`` -1
THEN AutoSimpHyp Auto (-1)
THEN HypSubst' (-2) 0
THEN Subst' com-kind(L6) = com-kind(L10) ∈ Atom 0
THEN Repeat (AutoSplit)
THEN Auto
THEN Try ((EqCD THENL [RepeatFor 4 ((EqCD THEN Auto)); Id])⋅)
THEN Try ((BLemma `deliver-msg_functionality`⋅ THEN Auto))) }
1
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P]))@i
17. ||P5|| = ||P7|| ∈ ℤ@i
18. ∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q@i
19. m : ℕ@i
20. x : Id@i
21. G1 : LabeledDAG(pInTransit(P.M[P]))@i
22. G2 : LabeledDAG(pInTransit(P.M[P]))@i
23. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
24. L3 : ℤ × Id@i
25. L5 : Id@i
26. L6 : pCom(P.M[P])@i
27. L7 : ℤ × Id@i
28. L9 : Id@i
29. L10 : pCom(P.M[P])@i
30. L3 = L7 ∈ (ℤ × Id)
31. L5 = L9 ∈ Id
32. L6 = L10 ∈ pCom(P.M[P])
33. com-kind(L10) = "msg" ∈ Atom
⊢ system-equiv(P.M[P];deliver-msg(t;comm-msg(L6);L9;P5;G1);deliver-msg(t;comm-msg(L10);L9;P7;G2))
2
.....subterm..... T:t
2:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P]))@i
17. ||P5|| = ||P7|| ∈ ℤ@i
18. ∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q@i
19. m : ℕ@i
20. x : Id@i
21. G1 : LabeledDAG(pInTransit(P.M[P]))@i
22. G2 : LabeledDAG(pInTransit(P.M[P]))@i
23. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
24. L3 : ℤ × Id@i
25. L5 : Id@i
26. L6 : pCom(P.M[P])@i
27. L7 : ℤ × Id@i
28. L9 : Id@i
29. L10 : pCom(P.M[P])@i
30. L3 = L7 ∈ (ℤ × Id)
31. L5 = L9 ∈ Id
32. L6 = L10 ∈ pCom(P.M[P])
33. com-kind(L10) = "msg" ∈ Atom
34. system-equiv(P.M[P];deliver-msg(t;comm-msg(L6);L9;P5;G1);deliver-msg(t;comm-msg(L10);L9;P7;G2))
⊢ deliver-msg(t;comm-msg(L6);L9;P5;G1) = deliver-msg(t;comm-msg(L10);L9;P7;G2) ∈ (Top × LabeledDAG(pInTransit(P.M[P])))
3
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P]))@i
17. ||P5|| = ||P7|| ∈ ℤ@i
18. ∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q@i
19. m : ℕ@i
20. x : Id@i
21. G1 : LabeledDAG(pInTransit(P.M[P]))@i
22. G2 : LabeledDAG(pInTransit(P.M[P]))@i
23. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
24. L3 : ℤ × Id@i
25. L5 : Id@i
26. L6 : pCom(P.M[P])@i
27. L7 : ℤ × Id@i
28. L9 : Id@i
29. L10 : pCom(P.M[P])@i
30. com-kind(L10) ≠ "msg" ∈ Atom
31. L3 = L7 ∈ (ℤ × Id)
32. L5 = L9 ∈ Id
33. L6 = L10 ∈ pCom(P.M[P])
34. com-kind(L10) = "create" ∈ Atom
⊢ system-equiv(P.M[P];create-component(t;comm-create(L6);L9;P5;G1);create-component(t;comm-create(L10);L9;P7;G2))
4
.....subterm..... T:t
2:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P]))@i
17. ||P5|| = ||P7|| ∈ ℤ@i
18. ∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q@i
19. m : ℕ@i
20. x : Id@i
21. G1 : LabeledDAG(pInTransit(P.M[P]))@i
22. G2 : LabeledDAG(pInTransit(P.M[P]))@i
23. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
24. L3 : ℤ × Id@i
25. L5 : Id@i
26. L6 : pCom(P.M[P])@i
27. L7 : ℤ × Id@i
28. L9 : Id@i
29. L10 : pCom(P.M[P])@i
30. com-kind(L10) ≠ "msg" ∈ Atom
31. L3 = L7 ∈ (ℤ × Id)
32. L5 = L9 ∈ Id
33. L6 = L10 ∈ pCom(P.M[P])
34. com-kind(L10) = "create" ∈ Atom
35. system-equiv(P.M[P];create-component(t;comm-create(L6);L9;P5;G1);create-component(t;comm-create(L10);L9;P7;G2))
⊢ create-component(t;comm-create(L6);L9;P5;G1)
= create-component(t;comm-create(L10);L9;P7;G2)
∈ (Top × LabeledDAG(pInTransit(P.M[P])))
5
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P]))@i
17. ||P5|| = ||P7|| ∈ ℤ@i
18. ∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q@i
19. m : ℕ@i
20. x : Id@i
21. G1 : LabeledDAG(pInTransit(P.M[P]))@i
22. G2 : LabeledDAG(pInTransit(P.M[P]))@i
23. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
24. L3 : ℤ × Id@i
25. L5 : Id@i
26. L6 : pCom(P.M[P])@i
27. L7 : ℤ × Id@i
28. L9 : Id@i
29. L10 : pCom(P.M[P])@i
30. com-kind(L10) ≠ "new" ∈ Atom
31. com-kind(L10) ≠ "choose" ∈ Atom
32. com-kind(L10) ≠ "create" ∈ Atom
33. com-kind(L10) ≠ "msg" ∈ Atom
34. L3 = L7 ∈ (ℤ × Id)
35. L5 = L9 ∈ Id
36. L6 = L10 ∈ pCom(P.M[P])
⊢ system-equiv(P.M[P];<P5, G1>;<P7, G2>)
6
.....subterm..... T:t
2:n
1. M : Type ─→ Type
2. Continuous+(P.M[P])
3. nat2msg : ℕ ─→ pMsg(P.M[P])
4. loc2msg : Id ─→ pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : {1...}
10. ∀t:ℕt
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg) t)))
∧ ((pRun(S1;env;nat2msg;loc2msg) t)
= (pRun(S2;env;nat2msg;loc2msg) t)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P])))))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg)) ∈ (ℕ × ℕ × Id)
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. P6 = P8 ∈ LabeledDAG(pInTransit(P.M[P]))@i
17. ||P5|| = ||P7|| ∈ ℤ@i
18. ∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q@i
19. m : ℕ@i
20. x : Id@i
21. G1 : LabeledDAG(pInTransit(P.M[P]))@i
22. G2 : LabeledDAG(pInTransit(P.M[P]))@i
23. G1 = G2 ∈ LabeledDAG(pInTransit(P.M[P]))
24. L3 : ℤ × Id@i
25. L5 : Id@i
26. L6 : pCom(P.M[P])@i
27. L7 : ℤ × Id@i
28. L9 : Id@i
29. L10 : pCom(P.M[P])@i
30. com-kind(L10) ≠ "new" ∈ Atom
31. com-kind(L10) ≠ "choose" ∈ Atom
32. com-kind(L10) ≠ "create" ∈ Atom
33. com-kind(L10) ≠ "msg" ∈ Atom
34. L3 = L7 ∈ (ℤ × Id)
35. L5 = L9 ∈ Id
36. L6 = L10 ∈ pCom(P.M[P])
37. system-equiv(P.M[P];<P5, G1>;<P7, G2>)
⊢ <P5, G1> = <P7, G2> ∈ (Top × LabeledDAG(pInTransit(P.M[P])))
Latex:
Latex:
1. M : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. nat2msg : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])
4. loc2msg : Id {}\mrightarrow{} pMsg(P.M[P])
5. env : pEnvType(P.M[P])
6. S1 : System(P.M[P])
7. S2 : System(P.M[P])
8. system-equiv(P.M[P];S1;S2)
9. t : \{1...\}
10. \mforall{}t:\mBbbN{}t
(system-equiv(P.M[P];snd((pRun(S1;env;nat2msg;loc2msg) t));snd((pRun(S2;env;nat2msg;loc2msg)
t)))
\mwedge{} ((pRun(S1;env;nat2msg;loc2msg) t) = (pRun(S2;env;nat2msg;loc2msg) t)))@i
11. (env t pRun(S1;env;nat2msg;loc2msg)) = (env t pRun(S2;env;nat2msg;loc2msg))
12. P5 : component(P.M[P]) List@i
13. P6 : LabeledDAG(pInTransit(P.M[P]))@i
14. P7 : component(P.M[P]) List@i
15. P8 : LabeledDAG(pInTransit(P.M[P]))@i
16. (P6 = P8)
\mwedge{} (||P5|| = ||P7||)
\mwedge{} (\mforall{}k:\mBbbN{}||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z) \mwedge{} P\mequiv{}Q)@i
17. m : \mBbbN{}@i
18. x : Id@i
19. G1 : LabeledDAG(pInTransit(P.M[P]))@i
20. G2 : LabeledDAG(pInTransit(P.M[P]))@i
21. G1 = G2
22. L1 : pInTransit(P.M[P])@i
23. L2 : pInTransit(P.M[P])@i
24. L1 = L2
\mvdash{} system-equiv(P.M[P];snd(let ev,x@0,c = L1 in
if com-kind(c) =a "msg"
then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P5;G1)>
if com-kind(c) =a "create"
then <inr \mcdot{} , create-component(t;comm-create(c);x@0;P5;G1)>
if com-kind(c) =a "choose"
then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P5;G1)>
if com-kind(c) =a "new"
then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P5;G1)>
else <inr \mcdot{} , P5, G1>
fi );snd(let ev,x@0,c = L2 in
if com-kind(c) =a "msg"
then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P7;G2)>
if com-kind(c) =a "create"
then <inr \mcdot{} , create-component(t;comm-create(c);x@0;P7;G2)>
if com-kind(c) =a "choose"
then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P7;G2)>
if com-kind(c) =a "new"
then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P7;G2)>
else <inr \mcdot{} , P7, G2>
fi ))
\mwedge{} (let ev,x@0,c = L1 in
if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P5;G1)>
if com-kind(c) =a "create" then <inr \mcdot{} , create-component(t;comm-create(c);x@0;P5;G1)>
if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P5;G1)>
if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P5;G1)>
else <inr \mcdot{} , P5, G1>
fi
= let ev,x@0,c = L2 in
if com-kind(c) =a "msg" then <inl <ev, x@0, comm-msg(c)>, deliver-msg(t;comm-msg(c);x@0;P7;G2)>
if com-kind(c) =a "create" then <inr \mcdot{} , create-component(t;comm-create(c);x@0;P7;G2)>
if com-kind(c) =a "choose" then <inl <ev, x@0, nat2msg m>, deliver-msg(t;nat2msg m;x@0;P7;G2)>
if com-kind(c) =a "new" then <inl <ev, x@0, loc2msg x>, deliver-msg(t;loc2msg x;x@0;P7;G2)>
else <inr \mcdot{} , P7, G2>
fi )
By
Latex:
(RepeatFor 2 (D (-3))
THEN (RepeatFor 2 (D (-2)) THEN Reduce 0)
THEN RepUR ``pInTransit`` -1
THEN AutoSimpHyp Auto (-1)
THEN HypSubst' (-2) 0
THEN Subst' com-kind(L6) = com-kind(L10) 0
THEN Repeat (AutoSplit)
THEN Auto
THEN Try ((EqCD THENL [RepeatFor 4 ((EqCD THEN Auto)); Id])\mcdot{})
THEN Try ((BLemma `deliver-msg\_functionality`\mcdot{} THEN Auto)))
Home
Index