Step
*
1
2
2
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. P2 : System(P.M[P])@i
13. P4 : System(P.M[P])@i
14. system-equiv(P.M[P];P2;P4)@i
15. n : ℕ@i
16. m : ℕ@i
17. x : Id@i
⊢ system-equiv(P.M[P];snd(do-chosen-command(nat2msg;loc2msg;t;P2;n;m;x));
snd(do-chosen-command(nat2msg;loc2msg;t;P4;n;m;x)))
∧ (do-chosen-command(nat2msg;loc2msg;t;P2;n;m;x)
= do-chosen-command(nat2msg;loc2msg;t;P4;n;m;x)
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
BY
{ (DVar `P2'
THEN DVar `P4'
THEN RepUR ``system-equiv`` -4
THEN RepUR ``do-chosen-command`` 0
THEN RepeatFor 2 (AutoSplit)) }
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])))
∧ (||P5|| = ||P7|| ∈ ℤ)
∧ (∀k:ℕ||P5||. let x,P = P5[k] in let z,Q = P7[k] in (x = z ∈ Id) ∧ P≡Q)@i
17. n : ℕ@i
18. m : ℕ@i
19. x : Id@i
20. ↑lg-is-source(P6;n)
21. ↑lg-is-source(P8;n)
⊢ system-equiv(P.M[P];snd(let ev,x@0,c = lg-label(P6;n) in
let G' = lg-remove(P6;n) in
if com-kind(c) =a "msg"
then let ms = comm-msg(c) in
<inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>
if com-kind(c) =a "create"
then let P = comm-create(c) in
<inr ⋅ , create-component(t;P;x@0;P5;G')>
if com-kind(c) =a "choose"
then let ms = nat2msg m in
<inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>
if com-kind(c) =a "new"
then let ms = loc2msg x in
<inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>
else <inr ⋅ , P5, G'>
fi );snd(let ev,x@0,c = lg-label(P8;n) in
let G' = lg-remove(P8;n) in
if com-kind(c) =a "msg"
then let ms = comm-msg(c) in
<inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>
if com-kind(c) =a "create"
then let P = comm-create(c) in
<inr ⋅ , create-component(t;P;x@0;P7;G')>
if com-kind(c) =a "choose"
then let ms = nat2msg m in
<inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>
if com-kind(c) =a "new"
then let ms = loc2msg x in
<inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>
else <inr ⋅ , P7, G'>
fi ))
∧ (let ev,x@0,c = lg-label(P6;n) in
let G' = lg-remove(P6;n) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>
if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x@0;P5;G')>
if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>
if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P5;G')>
else <inr ⋅ , P5, G'>
fi
= let ev,x@0,c = lg-label(P8;n) in
let G' = lg-remove(P8;n) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>
if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x@0;P7;G')>
if com-kind(c) =a "choose" then let ms = nat2msg m in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>
if com-kind(c) =a "new" then let ms = loc2msg x in <inl <ev, x@0, ms>, deliver-msg(t;ms;x@0;P7;G')>
else <inr ⋅ , P7, G'>
fi
∈ (ℤ × Id × Id × pMsg(P.M[P])? × Top × LabeledDAG(pInTransit(P.M[P]))))
2
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. n : ℕ@i
18. ¬↑lg-is-source(P8;n)
19. ¬↑lg-is-source(P6;n)
20. m : ℕ@i
21. x : Id@i
⊢ system-equiv(P.M[P];<P5, P6>;<P7, P8>)
∧ (<inr ⋅ , P5, P6> = <inr ⋅ , P7, P8> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × 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. P2 : System(P.M[P])@i
13. P4 : System(P.M[P])@i
14. system-equiv(P.M[P];P2;P4)@i
15. n : \mBbbN{}@i
16. m : \mBbbN{}@i
17. x : Id@i
\mvdash{} system-equiv(P.M[P];snd(do-chosen-command(nat2msg;loc2msg;t;P2;n;m;x));
snd(do-chosen-command(nat2msg;loc2msg;t;P4;n;m;x)))
\mwedge{} (do-chosen-command(nat2msg;loc2msg;t;P2;n;m;x) = do-chosen-command(nat2msg;loc2msg;t;P4;n;m;x))
By
Latex:
(DVar `P2'
THEN DVar `P4'
THEN RepUR ``system-equiv`` -4
THEN RepUR ``do-chosen-command`` 0
THEN RepeatFor 2 (AutoSplit))
Home
Index