---

Step * 1 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. 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')])
BY
{ (InstHyp [⌈e'⌉;⌈v⌉] (-10)⋅ THEN Auto) }

---

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.  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{}  (\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
16.  e  :  E@i
17.  \mforall{}v:Interface
            ((correct  loc(e))
            {}\mRightarrow{}  v  \mmember{}  local-simulation-class(X;locs;hdr)(e)
            {}\mRightarrow{}  True
            {}\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'))))))))
18.  correct  loc(e)@i
19.  v  :  Interface@i
20.  v  \mmember{}  local-simulation-class(X;locs;hdr)(e)@i
21.  e'  :  E
22.  (e'  <loc  e)
23.  \muparrow{}has-header-and-in-locs(info(e');hdr;locs)
24.  R  v  (snd(msg-body(info(e'))))
\mvdash{}  \mdownarrow{}\mexists{}e':E.  ((e'  <  e)  \mwedge{}  R'[v;info(e')])


By

---

Latex:
(InstHyp  [\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]  (-10)\mcdot{}  THEN  Auto)

---

Home Index