---

Step * of Lemma local-simulation-validity2

∀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)))
          ⇒ (∀R:Interface ─→ Message(g) ─→ ℙ. ∀R':Interface ─→ Message(f) ─→ ℙ.
                ((∀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]))
                ⇒ (∀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')]))))
                ⇒ 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]))) 
        supposing hdr encodes Id × Message(g)))
BY
{ (InstLemma `local-simulation-validity` []
   THEN RepeatFor 7 ((ParallelLast' THENA Auto))
   THEN ((Intro THEN D -2) THENA Auto)
   THEN RepeatFor 3 ((ParallelLast' THENA Auto))
   THEN (With ⌈λ2x.True⌉ (D (-1))⋅ THENA Auto)
   THEN ((ParallelLast' THEN (D 0 THENA Auto))
         THEN (ParallelOp -2
               THENA (RepUR ``so_apply so_lambda`` 0
                      THEN RepeatFor 2 ((ParallelLast' THENA Auto))
                      THEN UnfoldTopAb (-1)
                      THEN RepeatFor 3 (ParallelLast)
                      THEN Auto)
               )
         )
   THEN (D 0
         THENA (Auto
                THEN (RWO "assert-has-header-and-in-locs" (-1) THENA Auto)
                THEN (Assert msg-body(info(e)) ∈ Id × Message(g) BY
                            Auto)
                THEN 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. [%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]

---

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{}R:Interface  {}\mrightarrow{}  Message(g)  {}\mrightarrow{}  \mBbbP{}.  \mforall{}R':Interface  {}\mrightarrow{}  Message(f)  {}\mrightarrow{}  \mBbbP{}.
                                ((\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]))
                                {}\mRightarrow{}  (\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')]))))
                                {}\mRightarrow{}  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]))) 
                supposing  hdr  encodes  Id  \mtimes{}  Message(g)))


By

---

Latex:
(InstLemma  `local-simulation-validity`  []
  THEN  RepeatFor  7  ((ParallelLast'  THENA  Auto))
  THEN  ((Intro  THEN  D  -2)  THENA  Auto)
  THEN  RepeatFor  3  ((ParallelLast'  THENA  Auto))
  THEN  (With  \mkleeneopen{}\mlambda{}\msubtwo{}x.True\mkleeneclose{}  (D  (-1))\mcdot{}  THENA  Auto)
  THEN  ((ParallelLast'  THEN  (D  0  THENA  Auto))
              THEN  (ParallelOp  -2
                          THENA  (RepUR  ``so\_apply  so\_lambda``  0
                                        THEN  RepeatFor  2  ((ParallelLast'  THENA  Auto))
                                        THEN  UnfoldTopAb  (-1)
                                        THEN  RepeatFor  3  (ParallelLast)
                                        THEN  Auto)
                          )
              )
  THEN  (D  0
              THENA  (Auto
                            THEN  (RWO  "assert-has-header-and-in-locs"  (-1)  THENA  Auto)
                            THEN  (Assert  msg-body(info(e))  \mmember{}  Id  \mtimes{}  Message(g)  BY
                                                    Auto)
                            THEN  Auto)
              ))

---

Home Index