---

Step * 1 1 of Lemma local-simulation-E-subtype


1. f : Name ─→ Type
2. Info : Type
3. es : EO+(Message(f))
4. hdr : Name
5. locs : bag(Id)
6. hdr encodes Id × Info
7. e1 : E
8. global-eo(local-simulation-inputs(es;e1;hdr;locs)) ∈ EO+(Info)
9. e2 : E
10. e1 ≤loc e2 @i
11. x : ℕ||local-simulation-inputs(es;e1;hdr;locs)||@i
12. True@i
13. ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List)
⊢ x ∈ ℕ||local-simulation-inputs(es;e2;hdr;locs)||
BY
{ ((InstHyp [⌈e1⌉] (-1)⋅ THENA Auto) THEN (InstHyp [⌈e2⌉] (-2)⋅ THENA Auto)) }

1
1. f : Name ─→ Type
2. Info : Type
3. es : EO+(Message(f))
4. hdr : Name
5. locs : bag(Id)
6. hdr encodes Id × Info
7. e1 : E
8. global-eo(local-simulation-inputs(es;e1;hdr;locs)) ∈ EO+(Info)
9. e2 : E
10. e1 ≤loc e2 @i
11. x : ℕ||local-simulation-inputs(es;e1;hdr;locs)||@i
12. True@i
13. ∀[e:E]. (local-simulation-inputs(es;e;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List)
14. local-simulation-inputs(es;e1;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List
15. local-simulation-inputs(es;e2;hdr;locs) ∈ ({i:Id| i ↓∈ locs}  × Info) List
⊢ x ∈ ℕ||local-simulation-inputs(es;e2;hdr;locs)||

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type
2.  Info  :  Type
3.  es  :  EO+(Message(f))
4.  hdr  :  Name
5.  locs  :  bag(Id)
6.  hdr  encodes  Id  \mtimes{}  Info
7.  e1  :  E
8.  global-eo(local-simulation-inputs(es;e1;hdr;locs))  \mmember{}  EO+(Info)
9.  e2  :  E
10.  e1  \mleq{}loc  e2  @i
11.  x  :  \mBbbN{}||local-simulation-inputs(es;e1;hdr;locs)||@i
12.  True@i
13.  \mforall{}[e:E].  (local-simulation-inputs(es;e;hdr;locs)  \mmember{}  (\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}    \mtimes{}  Info)  List)
\mvdash{}  x  \mmember{}  \mBbbN{}||local-simulation-inputs(es;e2;hdr;locs)||


By

---

Latex:
((InstHyp  [\mkleeneopen{}e1\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}e2\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto))

---

Home Index