---

Step * 1 of Lemma global-order-pairwise-compat-msg-interface-constraint

.....assertion..... 
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. LocalClass(X)@i'
⊢ ∃P:Id ─→ Message(f) List+ ─→ ℙ
   ∃R:Id ─→ Id ─→ Message(f) List+ ─→ Message(f) List+ ─→ ℙ
    ∀eo:EO+(Message(f))
      (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2]) eo ⇐⇒ eo-msg-interface-constraint(eo;X;hdrs;f))
BY
{ (D -1
   THEN (With ⌈λi,mss. (msg-header(last(mss)) ∈ hdrs)⌉ (D 0)⋅ THEN Auto)
   THEN With ⌈λi,j,mss1,mss2. ∃delay:ℤ
                               make-msg-interface(delay;j;last(mss2)) ↓∈ snd(F i*(firstn(||mss1|| 
                               - 1;mss1))(last(mss1)))⌉
   (D 0)⋅
   THEN RepUR ``so_apply`` 0
   THEN Auto
   THEN RepUR ``squash-causal-invariant eo-msg-interface-constraint es-local-property es-local-relation so_apply`` 0
   THEN RepUR ``squash-causal-invariant eo-msg-interface-constraint es-local-property es-local-relation so_apply`` -1
   THEN ParallelLast
   THEN (Assert ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e)) BY
               (Auto
                THEN Unfold `es-le-before` 0
                THEN (RWO "map_append_sq" 0 THENA Auto)
                THEN Reduce 0
                THEN (RWO "last_append" 0 THENA Auto)
                THEN RepUR ``last`` 0
                THEN Auto))
   THEN (InstHyp [⌈e⌉] (-1)⋅ THENA Auto)
   THEN RWW "-1" 0
   THEN RWW "-1" (-3)
   THEN (ParallelOp -3 THENA Auto)
   THEN ParallelLast) }

1
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E
     ((msg-header(last(map(λx.info(x);≤loc(e)))) ∈ hdrs)
     ⇒ (↓∃e':E
           ((e' < e)
           ∧ (∃delay:ℤ
               make-msg-interface(delay;loc(e);last(map(λx.info(x);≤loc(e)))) ↓∈ snd(F 
                                                                                     loc(e')*(firstn(||map(λx.info(x);
                                                                                                           ≤loc(e'))|| 
               - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (header(e) ∈ hdrs)@i
12. ∃e':E
     ((e' < e)
     ∧ (∃delay:ℤ
         make-msg-interface(delay;loc(e);info(e)) ↓∈ snd(F loc(e')*(firstn(||map(λx.info(x);≤loc(e'))|| 
         - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))))
⊢ ∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))

2
1. f : Name ─→ Type@i'
2. hdrs : Name List@i
3. X : EClass(Interface)@i'
4. F : Id ─→ hdataflow(Message(f);Interface)@i'
5. ∀es:EO+(Message(f)). ∀e:E.  (X(e) = (snd(F loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(Interface))@i'
6. eo : EO+(Message(f))@i'
7. ∀e:E. ((header(e) ∈ hdrs) ⇒ (↓∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))))@i
8. e : E@i
9. ∀e:E. (last(map(λx.info(x);≤loc(e))) ~ info(e))
10. last(map(λx.info(x);≤loc(e))) ~ info(e)
11. (msg-header(info(e)) ∈ hdrs)@i
12. ∃e':E. ∃delay:ℤ. ((e' < e) ∧ make-msg-interface(delay;loc(e);info(e)) ∈ X(e'))
⊢ ∃e':E
   ((e' < e)
   ∧ (∃delay:ℤ
       make-msg-interface(delay;loc(e);info(e)) ↓∈ snd(F loc(e')*(firstn(||map(λx.info(x);≤loc(e'))|| 
       - 1;map(λx.info(x);≤loc(e'))))(last(map(λx.info(x);≤loc(e')))))))

---

Latex:

---

Latex:
.....assertion..... 
1.  f  :  Name  {}\mrightarrow{}  Type@i'
2.  hdrs  :  Name  List@i
3.  X  :  EClass(Interface)@i'
4.  LocalClass(X)@i'
\mvdash{}  \mexists{}P:Id  {}\mrightarrow{}  Message(f)  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}
      \mexists{}R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Message(f)  List\msupplus{}  {}\mrightarrow{}  Message(f)  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}
        \mforall{}eo:EO+(Message(f))
            (squash-causal-invariant(i,L.P[i;L];a,b,L1,L2.R[a;b;L1;L2])  eo
            \mLeftarrow{}{}\mRightarrow{}  eo-msg-interface-constraint(eo;X;hdrs;f))


By

---

Latex:
(D  -1
  THEN  (With  \mkleeneopen{}\mlambda{}i,mss.  (msg-header(last(mss))  \mmember{}  hdrs)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
  THEN  With  \mkleeneopen{}\mlambda{}i,j,mss1,mss2.  \mexists{}delay:\mBbbZ{}
                                                          make-msg-interface(delay;j;last(mss2))  \mdownarrow{}\mmember{}  snd(F  i*(firstn(||mss1|| 
                                                          -  1;mss1))(last(mss1)))\mkleeneclose{}
  (D  0)\mcdot{}
  THEN  RepUR  ``so\_apply``  0
  THEN  Auto
  THEN  ...
  THEN  ...
  THEN  ParallelLast
  THEN  (Assert  \mforall{}e:E.  (last(map(\mlambda{}x.info(x);\mleq{}loc(e)))  \msim{}  info(e))  BY
                          (Auto
                            THEN  Unfold  `es-le-before`  0
                            THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  (RWO  "last\_append"  0  THENA  Auto)
                            THEN  RepUR  ``last``  0
                            THEN  Auto))
  THEN  (InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  RWW  "-1"  0
  THEN  RWW  "-1"  (-3)
  THEN  (ParallelOp  -3  THENA  Auto)
  THEN  ParallelLast)

---

Home Index