---

Step * 1 of Lemma local-simulation-validity2


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. [%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. R : Interface ─→ Message(g) ─→ ℙ@i'
13. R' : Interface ─→ Message(f) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
      (eo-msg-interface-constraint(eo;X;hdrs;g)
      ⇒ for every v in X there is an
         earlier event  with info=m such that
         R[v;m])@i'
15. ∀e:E. ∀v:Interface.
      ((correct loc(e))
      ⇒ v ∈ local-simulation-class(X;locs;hdr)(e)
      ⇒ λ2x.True[v]
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (↑has-header-and-in-locs(info(e');hdr;locs)) ∧ R[v;snd(msg-body(info(e')))])))
16. ∀e:E. ∀v:Interface.
      ((correct loc(e))
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ R[v;snd(msg-body(info(e)))]
      ⇒ (↓∃e':E. ((e' < e) ∧ R'[v;info(e')])))@i
⊢ for every v in local-simulation-class(X;locs;hdr) at location i s.t. correct i there is an earlier event with info=m
   such that R'[v;m]
BY
{ (RepUR ``so_apply so_lambda`` -2
   THEN UnfoldTopAb 0
   THEN ParallelOp -2
   THEN Thin (-4)
   THEN Auto
   THEN (InstHyp [⌈v⌉] (-4)⋅ THEN Auto)
   THEN SqExRepD) }

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. R : Interface ─→ Message(g) ─→ ℙ@i'
13. R' : Interface ─→ Message(f) ─→ ℙ@i'
14. ∀eo:EO+(Message(g))
      (eo-msg-interface-constraint(eo;X;hdrs;g)
      ⇒ for every v in X there is an
         earlier event  with info=m such that
         R[v;m])@i'
15. ∀e:E. ∀v:Interface.
      ((correct loc(e))
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ R[v;snd(msg-body(info(e)))]
      ⇒ (↓∃e':E. ((e' < e) ∧ R'[v;info(e')])))@i
16. e : E@i
17. ∀v:Interface
      ((correct loc(e))
      ⇒ v ∈ local-simulation-class(X;locs;hdr)(e)
      ⇒ True
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (↑has-header-and-in-locs(info(e');hdr;locs)) ∧ (R v (snd(msg-body(info(e'))))))))
18. correct loc(e)@i
19. v : Interface@i
20. v ∈ local-simulation-class(X;locs;hdr)(e)@i
21. e' : E
22. (e' <loc e)
23. ↑has-header-and-in-locs(info(e');hdr;locs)
24. R v (snd(msg-body(info(e'))))
⊢ ↓∃e':E. ((e' < e) ∧ R'[v;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.  [\%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.  R  :  Interface  {}\mrightarrow{}  Message(g)  {}\mrightarrow{}  \mBbbP{}@i'
13.  R'  :  Interface  {}\mrightarrow{}  Message(f)  {}\mrightarrow{}  \mBbbP{}@i'
14.  \mforall{}eo:EO+(Message(g))
            (eo-msg-interface-constraint(eo;X;hdrs;g)
            {}\mRightarrow{}  for  every  v  in  X  there  is  an
                  earlier  event    with  info=m  such  that
                  R[v;m])@i'
15.  \mforall{}e:E.  \mforall{}v:Interface.
            ((correct  loc(e))
            {}\mRightarrow{}  v  \mmember{}  local-simulation-class(X;locs;hdr)(e)
            {}\mRightarrow{}  \mlambda{}\msubtwo{}x.True[v]
            {}\mRightarrow{}  (\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')))])))
16.  \mforall{}e:E.  \mforall{}v:Interface.
            ((correct  loc(e))
            {}\mRightarrow{}  (\muparrow{}has-header-and-in-locs(info(e);hdr;locs))
            {}\mRightarrow{}  R[v;snd(msg-body(info(e)))]
            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  R'[v;info(e')])))@i
\mvdash{}  for  every  v  in  local-simulation-class(X;locs;hdr)  at  location  i  s.t.  correct  i
    there  is  an  earlier  event  with  info=m    such  that  R'[v;m]


By

---

Latex:
(RepUR  ``so\_apply  so\_lambda``  -2
  THEN  UnfoldTopAb  0
  THEN  ParallelOp  -2
  THEN  Thin  (-4)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}v\mkleeneclose{}]  (-4)\mcdot{}  THEN  Auto)
  THEN  SqExRepD)

---

Home Index