Step
*
1
1
1
1
1
1
1
of Lemma
local-simulation-validity
.....wf.....
1. correct : Id ─→ ℙ@i'
2. g : Name ─→ Type@i'
3. f : Name ─→ Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id × Message(g)
9. hdrs : Name List@i
10. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
⇒ (∀e:E. ∀v:Interface. (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. R[v;info(e')]
23. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
25. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
⊢ filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e)) ∈ {e:E| msg-header(info(e)) = hdr ∈ Name} List
BY
{ SubsumeC ⌈{e:E| ↑((λx.has-header-and-in-locs(info(x);hdr;locs)) e)} List⌉⋅ }
1
1. correct : Id ─→ ℙ@i'
2. g : Name ─→ Type@i'
3. f : Name ─→ Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id × Message(g)
9. hdrs : Name List@i
10. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
⇒ (∀e:E. ∀v:Interface. (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. R[v;info(e')]
23. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
25. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
⊢ filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e)) ∈ {e:E|
↑((λx.has-header-and-in-locs(info(x);hdr;locs)) e)} \000CList
2
1. correct : Id ─→ ℙ@i'
2. g : Name ─→ Type@i'
3. f : Name ─→ Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id × Message(g)
9. hdrs : Name List@i
10. es : EO+(Message(f))@i'
11. ∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface ─→ ℙ@i'
13. R : Interface ─→ Message(g) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
⇒ (∀e:E. ∀v:Interface. (v ∈ X(e) ⇒ P[v] ⇒ (↓∃e':E. ((e' < e) ∧ R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. ↑has-header-and-in-locs(info(e);hdr;locs)
19. v ∈ X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : {e:ℕ||local-simulation-inputs(es;e;hdr;locs)||| True}
22. R[v;info(e')]
23. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
25. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
27. filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))
= filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))
∈ ({e:E| ↑((λx.has-header-and-in-locs(info(x);hdr;locs)) e)} List)
⊢ ({e:E| ↑((λx.has-header-and-in-locs(info(x);hdr;locs)) e)} List) ⊆r ({e:E| msg-header(info(e)) = hdr ∈ Name} List)
Latex:
Latex:
.....wf.....
1. correct : Id {}\mrightarrow{} \mBbbP{}@i'
2. g : Name {}\mrightarrow{} Type@i'
3. f : Name {}\mrightarrow{} Type@i'
4. X : EClass(Interface)@i'
5. LocalClass(X)@i'
6. locs : bag(Id)@i
7. hdr : Name@i
8. hdr encodes Id \mtimes{} Message(g)
9. hdrs : Name List@i
10. es : EO+(Message(f))@i'
11. \mforall{}i:Id. ((correct i) {}\mRightarrow{} local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i))@i
12. P : Interface {}\mrightarrow{} \mBbbP{}@i'
13. R : Interface {}\mrightarrow{} Message(g) {}\mrightarrow{} \mBbbP{}@i'
14. \mforall{}eo:EO+(Message(g))
(eo-msg-interface-constraint(eo;X;hdrs;g)
{}\mRightarrow{} (\mforall{}e:E. \mforall{}v:Interface. (v \mmember{} X(e) {}\mRightarrow{} P[v] {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} R[v;info(e')])))))@i'
15. e : E@i
16. v : Interface@i
17. correct loc(e)@i
18. \muparrow{}has-header-and-in-locs(info(e);hdr;locs)
19. v \mmember{} X(local-simulation-event(es;e;hdr;locs))
20. P[v]@i
21. e' : \{e:\mBbbN{}||local-simulation-inputs(es;e;hdr;locs)||| True\}
22. R[v;info(e')]
23. (filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
24. \muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);
before(e))[e']);hdr;locs)
25. (filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
26. \muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);
before(e))[e']);hdr;locs)
\mvdash{} filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e)) \mmember{} \{e:E| msg-header(info(e)) = hdr\} \000CList
By
Latex:
SubsumeC \mkleeneopen{}\{e:E| \muparrow{}((\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs)) e)\} List\mkleeneclose{}\mcdot{}
Home
Index