---

Step * 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
22. (e' < local-simulation-event(es;e;hdr;locs))
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
{ (Unfold `local-simulation-eo` -2
   THEN (RWO "global-eo-causl" (-2) THENA Using [`Info',⌈Message(g)⌉] Auto⋅)
   THEN RepUR ``local-simulation-eo`` (-3)
   ⋅
   THEN (RWO "global-eo-E-sq" (-3) THENA Auto)
   THEN Unfold `local-simulation-event` -2
   THEN (RWW "filter-map length-map" (-2) THENA Auto)
   THEN RepUR ``compose`` -2) }

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. 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')))])

---

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
22.  (e'  <  local-simulation-event(es;e;hdr;locs))
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:
(Unfold  `local-simulation-eo`  -2
  THEN  (RWO  "global-eo-causl"  (-2)  THENA  Using  [`Info',\mkleeneopen{}Message(g)\mkleeneclose{}]  Auto\mcdot{})
  THEN  RepUR  ``local-simulation-eo``  (-3)
  \mcdot{}
  THEN  (RWO  "global-eo-E-sq"  (-3)  THENA  Auto)
  THEN  Unfold  `local-simulation-event`  -2
  THEN  (RWW  "filter-map  length-map"  (-2)  THENA  Auto)
  THEN  RepUR  ``compose``  -2)

---

Home Index