---

Step * 1 of Lemma local-simulation-msg-constraint


1. f : Name ⟶ Type
2. g : Name ⟶ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
⊢ ↓∃e':E. ∃delay:ℤ. ((e' < j) ∧ make-msg-interface(delay;loc(j);info(j)) ∈ X(e'))
BY
{ ((Assert filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e 
          ∧ (↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)) BY
          (RepeatFor 2 (Thin (-1))
           THEN MoveToConcl (-1)
           THEN (GenConcl ⌜≤loc(e) = L ∈ ({a:E| a ≤loc e }  List)⌝ ⋅ THENA Auto)
           THEN ((GenConcl ⌜filter(λx.has-header-and-in-locs(info(x);hdr;locs);L)
                            = FL
                            ∈ ({x:{a:E| a ≤loc e } | ↑((λx.has-header-and-in-locs(info(x);hdr;locs)) x)}  List)⌝⋅
                  THENA Auto
                  )
                 THEN Thin (-1)
                 THEN Reduce (-1)
                 THEN (D 0 THENA Auto)
                 THEN (GenConclTerm ⌜FL[j]⌝⋅ THENA Auto)
                 THEN Thin (-1)
                 THEN D -1
                 THEN Auto)))
   THEN Unfold `local-simulation-input-validity` -8
   THEN (InstHyp [⌜filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]⌝] (-8)⋅ THENA Auto)
   THEN SqExRepD) }

1
1. f : Name ⟶ Type
2. g : Name ⟶ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
      ((loc(e) = i ∈ Id)
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e 
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
⊢ (msg-header(snd(msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]))) ∈ hdrs)

2
1. f : Name ⟶ Type
2. g : Name ⟶ Type
3. X : EClass(Interface)
4. LocalClass(X)
5. es : EO+(Message(f))
6. hdr : Name
7. locs : bag(Id)
8. hdr encodes Id × Message(g)
9. hdrs : Name List
10. i : Id
11. ∀e:E
      ((loc(e) = i ∈ Id)
      ⇒ (↑has-header-and-in-locs(info(e);hdr;locs))
      ⇒ (msg-header(snd(msgval(e))) ∈ hdrs)
      ⇒ (↓∃e':E. ((e' <loc e) ∧ (∃del:ℤ. <del, msgval(e)> ∈ local-simulation-class(X;locs;hdr)(e')))))@i
12. e : E@i
13. loc(e) = i ∈ Id@i
14. local-simulation-eo(es;e;hdr;locs) ∈ EO+(Message(g))
15. j : ℕ||filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))||@i
16. (header(j) ∈ hdrs)@i
17. j ∈ E
18. filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j] ≤loc e 
19. ↑has-header-and-in-locs(info(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j]);hdr;locs)
20. e' : E
21. (e' <loc filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])
22. del : ℤ
23. <del, msgval(filter(λx.has-header-and-in-locs(info(x);hdr;locs);≤loc(e))[j])> ∈
     local-simulation-class(X;locs;hdr)(e')
⊢ ↓∃e':E. ∃delay:ℤ. ((e' < j) ∧ make-msg-interface(delay;loc(j);info(j)) ∈ X(e'))

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  g  :  Name  {}\mrightarrow{}  Type
3.  X  :  EClass(Interface)
4.  LocalClass(X)
5.  es  :  EO+(Message(f))
6.  hdr  :  Name
7.  locs  :  bag(Id)
8.  hdr  encodes  Id  \mtimes{}  Message(g)
9.  hdrs  :  Name  List
10.  i  :  Id
11.  local-simulation-input-validity(g;X;hdr;locs;hdrs;es;i)@i
12.  e  :  E@i
13.  loc(e)  =  i@i
14.  local-simulation-eo(es;e;hdr;locs)  \mmember{}  EO+(Message(g))
15.  j  :  \mBbbN{}||filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))||@i
16.  (header(j)  \mmember{}  hdrs)@i
17.  j  \mmember{}  E
\mvdash{}  \mdownarrow{}\mexists{}e':E.  \mexists{}delay:\mBbbZ{}.  ((e'  <  j)  \mwedge{}  make-msg-interface(delay;loc(j);info(j))  \mmember{}  X(e'))


By

---

Latex:
((Assert  filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j]  \mleq{}loc  e 
                \mwedge{}  (\muparrow{}has-header-and-in-locs(info(filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);
                                                                                              \mleq{}loc(e))[j]);hdr;locs))  BY
                (RepeatFor  2  (Thin  (-1))
                  THEN  MoveToConcl  (-1)
                  THEN  (GenConcl  \mkleeneopen{}\mleq{}loc(e)  =  L\mkleeneclose{}  \mcdot{}  THENA  Auto)
                  THEN  ((GenConcl  \mkleeneopen{}filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);L)  =  FL\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  Thin  (-1)
                              THEN  Reduce  (-1)
                              THEN  (D  0  THENA  Auto)
                              THEN  (GenConclTerm  \mkleeneopen{}FL[j]\mkleeneclose{}\mcdot{}  THENA  Auto)
                              THEN  Thin  (-1)
                              THEN  D  -1
                              THEN  Auto)))
  THEN  Unfold  `local-simulation-input-validity`  -8
  THEN  (InstHyp  [\mkleeneopen{}filter(\mlambda{}x.has-header-and-in-locs(info(x);hdr;locs);\mleq{}loc(e))[j]\mkleeneclose{}]  (-8)\mcdot{}  THENA  Auto)
  THEN  SqExRepD)

---

Home Index