---

Step * of Lemma local-simulation-validity

∀correct:Id ⟶ ℙ. ∀g,f:Name ⟶ Type. ∀X:EClass(Interface).
  (LocalClass(X)
  ⇒ (∀locs:bag(Id). ∀hdr:Name.
        ∀hdrs:Name List. ∀es:EO+(Message(f)).
          ((∀i:Id. ((correct i) ⇒ local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
          ⇒ (∀P:Interface ⟶ ℙ. ∀R:Interface ⟶ Message(g) ⟶ ℙ.
                ((∀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')]))))))
                ⇒ (∀e:E. ∀v:Interface.
                      ((correct loc(e))
                      ⇒ v ∈ local-simulation-class(X;locs;hdr)(e)
                      ⇒ P[v]
                      ⇒ (↓∃e':E
                            ((e' <loc e)
                            ∧ (↑has-header-and-in-locs(info(e');hdr;locs))
                            ∧ R[v;snd(msg-body(info(e')))]))))))) 
        supposing hdr encodes Id × Message(g)))
BY
{ (Auto
   THEN (RWO "local-simulation-classrel" (-2) THENA Auto)
   THEN (InstHyp [⌜local-simulation-eo(es;e;hdr;locs)⌝;⌜local-simulation-event(es;e;hdr;locs)⌝;⌜v⌝] (-6)⋅
         THENA (Using [`Info',⌜Message(g)⌝] Auto⋅
                THEN Using [`i', ⌜loc(e)⌝] (BLemma `local-simulation-msg-constraint`)⋅
                THEN Auto)
         )
   THEN D -1
   THEN ExRepD) }

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

---

Latex:

---

Latex:
\mforall{}correct:Id  {}\mrightarrow{}  \mBbbP{}.  \mforall{}g,f:Name  {}\mrightarrow{}  Type.  \mforall{}X:EClass(Interface).
    (LocalClass(X)
    {}\mRightarrow{}  (\mforall{}locs:bag(Id).  \mforall{}hdr:Name.
                \mforall{}hdrs:Name  List.  \mforall{}es:EO+(Message(f)).
                    ((\mforall{}i:Id.  ((correct  i)  {}\mRightarrow{}  local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)))
                    {}\mRightarrow{}  (\mforall{}P:Interface  {}\mrightarrow{}  \mBbbP{}.  \mforall{}R:Interface  {}\mrightarrow{}  Message(g)  {}\mrightarrow{}  \mBbbP{}.
                                ((\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')]))))))
                                {}\mRightarrow{}  (\mforall{}e:E.  \mforall{}v:Interface.
                                            ((correct  loc(e))
                                            {}\mRightarrow{}  v  \mmember{}  local-simulation-class(X;locs;hdr)(e)
                                            {}\mRightarrow{}  P[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')))]))))))) 
                supposing  hdr  encodes  Id  \mtimes{}  Message(g)))


By

---

Latex:
(Auto
  THEN  (RWO  "local-simulation-classrel"  (-2)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}local-simulation-eo(es;e;hdr;locs)\mkleeneclose{};\mkleeneopen{}local-simulation-event(es;e;hdr;locs)\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}
              ]  (-6)\mcdot{}
              THENA  (Using  [`Info',\mkleeneopen{}Message(g)\mkleeneclose{}]  Auto\mcdot{}
                            THEN  Using  [`i',  \mkleeneopen{}loc(e)\mkleeneclose{}]  (BLemma  `local-simulation-msg-constraint`)\mcdot{}
                            THEN  Auto)
              )
  THEN  D  -1
  THEN  ExRepD)

---

Home Index