---

Step * 1 1 of Lemma local-simulation-validity


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. e' < ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))||
23. R[v;info(e')]
⊢ ↓∃e':E. ((e' <loc e) ∧ (↑has-header-and-in-locs(info(e');hdr;locs)) ∧ R[v;snd(msg-body(info(e')))])
BY
{ Assert ⌜0 ≤ e'⌝⋅ }

1
.....assertion..... 
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. e' < ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))||
23. R[v;info(e')]
⊢ 0 ≤ e'

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. e' < ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))||
23. R[v;info(e')]
24. 0 ≤ e'
⊢ ↓∃e':E. ((e' <loc e) ∧ (↑has-header-and-in-locs(info(e');hdr;locs)) ∧ R[v;snd(msg-body(info(e')))])

---

Latex:

---

Latex:

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.  e'  <  ||filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))||
23.  R[v;info(e')]
\mvdash{}  \mdownarrow{}\mexists{}e':E
        ((e'  <loc  e)  \mwedge{}  (\muparrow{}has-header-and-in-locs(info(e');hdr;locs))  \mwedge{}  R[v;snd(msg-body(info(e')))])


By

---

Latex:
Assert  \mkleeneopen{}0  \mleq{}  e'\mkleeneclose{}\mcdot{}

---

Home Index