Step
*
1
1
1
1
1
of Lemma
reliable-env-property2
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ⟶ pMsg(P.M[P])@i
5. l2m : Id ⟶ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. reliable-env(env; pRun(S;env;n2m;l2m))@i
8. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
∃e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
9. t : {1...}
10. x : Id@i
11. [%12] : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
12. P : Process(P.M[P])@i
13. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
14. 0 < t
15. v1 : ℤ × Id@i
16. ms : pMsg(P.M[P])@i
17. v2 : Process(P.M[P])@i
18. G : LabeledDAG(Id × pCom(P.M[P]))@i
19. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
20. n : ℕlg-size(G)@i
21. v3 : Id@i
22. v4 : pCom(P.M[P])@i
23. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
24. (com-kind(v4) ∈ ``msg choose new``)@i
25. v5 : ℤ × Id × Id × pMsg(P.M[P])?@i
26. v7 : component(P.M[P]) List@i
27. v8 : LabeledDAG(pInTransit(P.M[P]))@i
28. (pRun(S;env;n2m;l2m) (t - 1)) = <v5, v7, v8> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
29. v9 : ℕ@i
30. v11 : ℕ@i
31. v12 : Id@i
32. (env t pRun(S;env;n2m;l2m)) = <v9, v11, v12> ∈ (ℕ × ℕ × Id)@i
33. ↑lg-is-source(v8;v9)
⊢ (P ∈ mapfilter(λc.(snd(c));λc.fst(c) = x;v7))
⇒ (↑let info,S = let ev,x,c = lg-label(v8;v9) in
let G' = lg-remove(v8;v9) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x;v7;G')>
if com-kind(c) =a "choose" then let ms = n2m v11 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "new" then let ms = l2m v12 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
else <inr ⋅ , v7, G'>
fi
in isl(info) ∧b let ev,z,m = outl(info) in x = z)
⇒ (let info,S = let ev,x,c = lg-label(v8;v9) in
let G' = lg-remove(v8;v9) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x;v7;G')>
if com-kind(c) =a "choose" then let ms = n2m v11 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "new" then let ms = l2m v12 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
else <inr ⋅ , v7, G'>
fi
in let ev,z,m = outl(info) in
<ev, m>
= <v1, ms>
∈ (ℤ × Id × pMsg(P.M[P])))
⇒ add-cause(<t, x>;G) ⊆ snd(snd(let ev,x,c = lg-label(v8;v9) in
let G' = lg-remove(v8;v9) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "create" then let P = comm-create(c) in <inr ⋅ , create-component(t;P;x;v7;G')>
if com-kind(c) =a "choose" then let ms = n2m v11 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "new" then let ms = l2m v12 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
else <inr ⋅ , v7, G'>
fi ))
BY
{ RepUR ``let`` 0 }
1
1. [M] : Type ⟶ Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : ℕ ⟶ pMsg(P.M[P])@i
5. l2m : Id ⟶ pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. reliable-env(env; pRun(S;env;n2m;l2m))@i
8. ∀tn:run-msg-commands(pRun(S;env;n2m;l2m))
∃e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in (run-info(pRun(S;env;n2m;l2m);e)
= intransit-to-info(n2m;l2m;pRun(S;env;n2m;l2m);env;run-event-step(e);run-command(pRun(S;env;n2m;l2m);t;n))
∈ (ℤ × Id × pMsg(P.M[P])))
∧ (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))) ∈ Id)
9. t : {1...}
10. x : Id@i
11. [%12] : ↑is-run-event(pRun(S;env;n2m;l2m);t;x)@i
12. P : Process(P.M[P])@i
13. (P ∈ run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
14. 0 < t
15. v1 : ℤ × Id@i
16. ms : pMsg(P.M[P])@i
17. v2 : Process(P.M[P])@i
18. G : LabeledDAG(Id × pCom(P.M[P]))@i
19. Process-apply(P;ms) = <v2, G> ∈ (Process(P.M[P]) × pExt(P.M[P]))@i
20. n : ℕlg-size(G)@i
21. v3 : Id@i
22. v4 : pCom(P.M[P])@i
23. lg-label(G;n) = <v3, v4> ∈ (Id × pCom(P.M[P]))@i
24. (com-kind(v4) ∈ ``msg choose new``)@i
25. v5 : ℤ × Id × Id × pMsg(P.M[P])?@i
26. v7 : component(P.M[P]) List@i
27. v8 : LabeledDAG(pInTransit(P.M[P]))@i
28. (pRun(S;env;n2m;l2m) (t - 1)) = <v5, v7, v8> ∈ (ℤ × Id × Id × pMsg(P.M[P])? × System(P.M[P]))@i
29. v9 : ℕ@i
30. v11 : ℕ@i
31. v12 : Id@i
32. (env t pRun(S;env;n2m;l2m)) = <v9, v11, v12> ∈ (ℕ × ℕ × Id)@i
33. ↑lg-is-source(v8;v9)
⊢ (P ∈ mapfilter(λc.(snd(c));λc.fst(c) = x;v7))
⇒ (↑let info,S = let ev,x,c = lg-label(v8;v9) in
if com-kind(c) =a "msg" then <inl <ev, x, comm-msg(c)>, deliver-msg(t;comm-msg(c);x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "choose" then <inl <ev, x, n2m v11>, deliver-msg(t;n2m v11;x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "new" then <inl <ev, x, l2m v12>, deliver-msg(t;l2m v12;x;v7;lg-remove(v8;v9))>
else <inr ⋅ , v7, lg-remove(v8;v9)>
fi
in isl(info) ∧b let ev,z,m = outl(info) in x = z)
⇒ (let info,S = let ev,x,c = lg-label(v8;v9) in
if com-kind(c) =a "msg" then <inl <ev, x, comm-msg(c)>, deliver-msg(t;comm-msg(c);x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "choose" then <inl <ev, x, n2m v11>, deliver-msg(t;n2m v11;x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "new" then <inl <ev, x, l2m v12>, deliver-msg(t;l2m v12;x;v7;lg-remove(v8;v9))>
else <inr ⋅ , v7, lg-remove(v8;v9)>
fi
in let ev,z,m = outl(info) in
<ev, m>
= <v1, ms>
∈ (ℤ × Id × pMsg(P.M[P])))
⇒ add-cause(<t, x>;G) ⊆ snd(snd(let ev,x,c = lg-label(v8;v9) in
if com-kind(c) =a "msg" then <inl <ev, x, comm-msg(c)>, deliver-msg(t;comm-msg(c);x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "create" then <inr ⋅ , create-component(t;comm-create(c);x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "choose" then <inl <ev, x, n2m v11>, deliver-msg(t;n2m v11;x;v7;lg-remove(v8;v9))>
if com-kind(c) =a "new" then <inl <ev, x, l2m v12>, deliver-msg(t;l2m v12;x;v7;lg-remove(v8;v9))>
else <inr ⋅ , v7, lg-remove(v8;v9)>
fi ))
Latex:
Latex:
1. [M] : Type {}\mrightarrow{} Type
2. Continuous+(P.M[P])
3. S : InitialSystem(P.M[P])@i
4. n2m : \mBbbN{} {}\mrightarrow{} pMsg(P.M[P])@i
5. l2m : Id {}\mrightarrow{} pMsg(P.M[P])@i
6. env : pEnvType(P.M[P])@i
7. reliable-env(env; pRun(S;env;n2m;l2m))@i
8. \mforall{}tn:run-msg-commands(pRun(S;env;n2m;l2m))
\mexists{}e:runEvents(pRun(S;env;n2m;l2m))
let t,n = tn
in ...
\mwedge{} (run-event-loc(e) = (fst(snd(run-command(pRun(S;env;n2m;l2m);t;n)))))
9. t : \{1...\}
10. x : Id@i
11. [\%12] : \muparrow{}is-run-event(pRun(S;env;n2m;l2m);t;x)@i
12. P : Process(P.M[P])@i
13. (P \mmember{} run-event-state-when(pRun(S;env;n2m;l2m);<t, x>))@i
14. 0 < t
15. v1 : \mBbbZ{} \mtimes{} Id@i
16. ms : pMsg(P.M[P])@i
17. v2 : Process(P.M[P])@i
18. G : LabeledDAG(Id \mtimes{} pCom(P.M[P]))@i
19. Process-apply(P;ms) = <v2, G>@i
20. n : \mBbbN{}lg-size(G)@i
21. v3 : Id@i
22. v4 : pCom(P.M[P])@i
23. lg-label(G;n) = <v3, v4>@i
24. (com-kind(v4) \mmember{} ``msg choose new``)@i
25. v5 : \mBbbZ{} \mtimes{} Id \mtimes{} Id \mtimes{} pMsg(P.M[P])?@i
26. v7 : component(P.M[P]) List@i
27. v8 : LabeledDAG(pInTransit(P.M[P]))@i
28. (pRun(S;env;n2m;l2m) (t - 1)) = <v5, v7, v8>@i
29. v9 : \mBbbN{}@i
30. v11 : \mBbbN{}@i
31. v12 : Id@i
32. (env t pRun(S;env;n2m;l2m)) = <v9, v11, v12>@i
33. \muparrow{}lg-is-source(v8;v9)
\mvdash{} (P \mmember{} mapfilter(\mlambda{}c.(snd(c));\mlambda{}c.fst(c) = x;v7))
{}\mRightarrow{} (\muparrow{}let info,S = let ev,x,c = lg-label(v8;v9) in
let G' = lg-remove(v8;v9) in
if com-kind(c) =a "msg"
then let ms = comm-msg(c) in
<inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "create"
then let P = comm-create(c) in
<inr \mcdot{} , create-component(t;P;x;v7;G')>
if com-kind(c) =a "choose"
then let ms = n2m v11 in
<inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "new" then let ms = l2m v12 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G'\000C)>
else <inr \mcdot{} , v7, G'>
fi
in isl(info) \mwedge{}\msubb{} let ev,z,m = outl(info) in x = z)
{}\mRightarrow{} (let info,S = let ev,x,c = lg-label(v8;v9) in
let G' = lg-remove(v8;v9) in
if com-kind(c) =a "msg"
then let ms = comm-msg(c) in
<inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
if com-kind(c) =a "create"
then let P = comm-create(c) in
<inr \mcdot{} , create-component(t;P;x;v7;G')>
if com-kind(c) =a "choose" then let ms = n2m v11 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;\000CG')>
if com-kind(c) =a "new" then let ms = l2m v12 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')\000C>
else <inr \mcdot{} , v7, G'>
fi
in let ev,z,m = outl(info) in
<ev, m>
= <v1, ms>)
{}\mRightarrow{} add-cause(<t, x>G) \msubseteq{} snd(snd(let ev,x,c = lg-label(v8;v9) in
let G' = lg-remove(v8;v9) in
if com-kind(c) =a "msg" then let ms = comm-msg(c) in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;\000CG')>
if com-kind(c) =a "create"
then let P = comm-create(c) in
<inr \mcdot{} , create-component(t;P;x;v7;G')>
if com-kind(c) =a "choose" then let ms = n2m v11 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G\000C')>
if com-kind(c) =a "new" then let ms = l2m v12 in <inl <ev, x, ms>, deliver-msg(t;ms;x;v7;G')>
else <inr \mcdot{} , v7, G'>
fi ))
By
Latex:
RepUR ``let`` 0
Home
Index