---

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 (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']
             ∈ filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))) BY
          Auto)
   THEN RWO "member_filter" (-1)
   THEN Auto
   THEN Reduce (-1)
   THEN (RWO "member-es-before" (-2) THENA Auto)) }

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')]
24. (filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e'] <loc e)
25. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']);hdr;locs)
⊢ ↓∃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  (filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))[e']
                      \mmember{}  filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e)))  BY
                Auto)
  THEN  RWO  "member\_filter"  (-1)
  THEN  Auto
  THEN  Reduce  (-1)
  THEN  (RWO  "member-es-before"  (-2)  THENA  Auto))

---

Home Index