Step
*
1
3
1
1
1
2
of Lemma
local-simulation-msg-constraint
1. f : Name ─→ Type
2. g : Name ─→ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
((loc(e) = i ∈ Id)
⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
22. del : ℤ
23. (↑has-header-and-in-locs(info(e');hdr;locs))
∧ <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
X(local-simulation-event(es;e';hdr;locs))
24. msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) ∈ Id × Message(g)
25. (e' <loc e)
26. E ⊆r E
27. λx.x ∈ E ─→ E
28. local-simulation-event(es;e';hdr;locs) ∈ E
⊢ ∃e':E. ∃delay:ℤ. ((e' < j) ∧ make-msg-interface(delay;loc(j);info(j)) ∈ X(e'))
BY
{ ((InstConcl [⌈local-simulation-event(es;e';hdr;locs)⌉;⌈del⌉]⋅ THENA Auto) THEN D 0) }
1
1. f : Name ─→ Type
2. g : Name ─→ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
((loc(e) = i ∈ Id)
⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
22. del : ℤ
23. (↑has-header-and-in-locs(info(e');hdr;locs))
∧ <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
X(local-simulation-event(es;e';hdr;locs))
24. msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) ∈ Id × Message(g)
25. (e' <loc e)
26. E ⊆r E
27. λx.x ∈ E ─→ E
28. local-simulation-event(es;e';hdr;locs) ∈ E
⊢ (local-simulation-event(es;e';hdr;locs) < j)
2
1. f : Name ─→ Type
2. g : Name ─→ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
((loc(e) = i ∈ Id)
⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
22. del : ℤ
23. (↑has-header-and-in-locs(info(e');hdr;locs))
∧ <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
X(local-simulation-event(es;e';hdr;locs))
24. msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) ∈ Id × Message(g)
25. (e' <loc e)
26. E ⊆r E
27. λx.x ∈ E ─→ E
28. local-simulation-event(es;e';hdr;locs) ∈ E
⊢ make-msg-interface(del;loc(j);info(j)) ∈ X(local-simulation-event(es;e';hdr;locs))
Latex:
Latex:
1. f : Name {}\mrightarrow{} Type
2. g : Name {}\mrightarrow{} Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id \mtimes{} Message(g)
9. hdrs : Name List
10. i : Id
11. \mforall{}e:E
((loc(e) = i)
{}\mRightarrow{} (\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
{}\mRightarrow{} (msg-header(snd(msgval(e))) \mmember{} hdrs)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' <loc e) \mwedge{} (\mexists{}del:\mBbbZ{}. <del, msgval(e)> \mmember{} local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i@i
14. local-simulation-eo(es;e;hdr;locs) \mmember{} EO+(Message(g))
15. j : \mBbbN{}||filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))||@i
16. (header(j) \mmember{} hdrs)@i
17. j \mmember{} E
18. filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j] \mleq{}loc e
19. \muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);
\mleq{}loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j])
22. del : \mBbbZ{}
23. (\muparrow{}has-header-and-in-locs(info(e');hdr;locs))
\mwedge{} <del, msgval(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j])> \mmember{}
X(local-simulation-event(es;e';hdr;locs))
24. msgval(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j]) \mmember{} Id \mtimes{} Message(g)
25. (e' <loc e)
26. E \msubseteq{}r E
27. \mlambda{}x.x \mmember{} E {}\mrightarrow{} E
28. local-simulation-event(es;e';hdr;locs) \mmember{} E
\mvdash{} \mexists{}e':E. \mexists{}delay:\mBbbZ{}. ((e' < j) \mwedge{} make-msg-interface(delay;loc(j);info(j)) \mmember{} X(e'))
By
Latex:
((InstConcl [\mkleeneopen{}local-simulation-event(es;e';hdr;locs)\mkleeneclose{};\mkleeneopen{}del\mkleeneclose{}]\mcdot{} THENA Auto) THEN D 0)
Home
Index