Step
*
1
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. local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)@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
⊢ ↓∃e':E. ∃delay:ℤ. ((e' < j) ∧ make-msg-interface(delay;loc(j);info(j)) ∈ X(e'))
BY
{ ((Assert filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e
∧ (↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)) BY
(RepeatFor 2 (Thin (-1))
THEN MoveToConcl (-1)
THEN (GenConcl ⌈≤loc(e) = L ∈ ({a:E| a ≤loc e } List)⌉ ⋅ THENA Auto)
THEN ((GenConcl ⌈filter(λx.has-header-and-in-locs(info(x);hdr;locs);L)
= FL
∈ ({x:{a:E| a ≤loc e } | ↑((λx.has-header-and-in-locs(info(x);hdr;locs)) x)} List)⌉⋅
THENA Auto
)
THEN Thin (-1)
THEN Reduce (-1)
THEN (D 0 THENA Auto)
THEN (GenConclTerm ⌈FL[j]⌉⋅ THENA Auto)
THEN Thin (-1)
THEN D -1
THEN Auto)))
THEN Unfold `local-simulation-input-validity` -8
THEN (InstHyp [⌈filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]⌉] (-8)⋅ THENA Auto)
THEN SqExRepD) }
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)
⊢ loc(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]) = i ∈ Id
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)
⊢ (msg-header(snd(msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]))) ∈ hdrs)
3
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. <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
local-simulation-class(X;locs;hdr)(e')
⊢ ↓∃e':E. ∃delay:ℤ. ((e' < j) ∧ make-msg-interface(delay;loc(j);info(j)) ∈ X(e'))
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. local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)@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
\mvdash{} \mdownarrow{}\mexists{}e':E. \mexists{}delay:\mBbbZ{}. ((e' < j) \mwedge{} make-msg-interface(delay;loc(j);info(j)) \mmember{} X(e'))
By
Latex:
((Assert filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j] \mleq{}loc e
\mwedge{} (\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)) BY
(RepeatFor 2 (Thin (-1))
THEN MoveToConcl (-1)
THEN (GenConcl \mkleeneopen{}\mleq{}loc(e) = L\mkleeneclose{} \mcdot{} THENA Auto)
THEN ((GenConcl \mkleeneopen{}filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);L) = FL\mkleeneclose{}\mcdot{} THENA Auto)
THEN Thin (-1)
THEN Reduce (-1)
THEN (D 0 THENA Auto)
THEN (GenConclTerm \mkleeneopen{}FL[j]\mkleeneclose{}\mcdot{} THENA Auto)
THEN Thin (-1)
THEN D -1
THEN Auto)))
THEN Unfold `local-simulation-input-validity` -8
THEN (InstHyp [\mkleeneopen{}filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j]\mkleeneclose{}] (-8)\mcdot{} THENA Auto)
THEN SqExRepD)
Home
Index