---

Step * 1 1 1 1 1 1 3 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. 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. L : {e:E| msg-header(info(e)) = hdr ∈ Name}  List@i
28. filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e)) = L ∈ ({e:E| msg-header(info(e)) = hdr ∈ Name}  List)@\000Ci
⊢ e' < ||L||
⇒ ((snd(msg-body(info(L[e']))))
   = (snd(map(λm.msg-body(m);map(λe.info(e);L))
     @ map(λm.msg-body(m);map(λe.info(e);if has-header-and-in-locs(info(e);hdr;locs) then [e] else [] fi ))[e']))
   ∈ Message(g))
BY
{ ((D 0 THENA Auto)
   THEN (RWW "select-append length-map map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN AutoSplit
   THEN (RWO "select-map" 0 THENA Auto)
   THEN Reduce 0) }

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)
27. L : {e:E| msg-header(info(e)) = hdr ∈ Name}  List@i
28. filter(λx.has-header-and-in-locs(info(x);hdr;locs);before(e)) = L ∈ ({e:E| msg-header(info(e)) = hdr ∈ Name}  List)@\000Ci
29. e' < ||L||@i
30. e' < ||L||
⊢ (snd(msg-body(info(L[e'])))) = (snd(msg-body(info(L[e'])))) ∈ Message(g)

---

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.  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)
27.  L  :  \{e:E|  msg-header(info(e))  =  hdr\}    List@i
28.  filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);before(e))  =  L@i
\mvdash{}  e'  <  ||L||
{}\mRightarrow{}  ((snd(msg-body(info(L[e']))))
      =  (snd(map(\mlambda{}m.msg-body(m);map(\mlambda{}e.info(e);L))
          @  map(\mlambda{}m.msg-body(m);map(\mlambda{}e.info(e);if  has-header-and-in-locs(info(e);hdr;locs)
                                                            then  [e]
                                                            else  []
                                                            fi  ))[e'])))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RWW  "select-append  length-map  map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  AutoSplit
  THEN  (RWO  "select-map"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index