---

Step * 1 2 1 of Lemma iseg-local-simulation-inputs


1. f : Name ─→ Type@i'
2. [Info] : Type
3. es : EO+(Message(f))@i'
4. hdr : Name@i
5. locs : bag(Id)@i
6. hdr encodes Id × Info
7. e1 : E@i
8. e2 : E@i
9. e1 ≤loc e2 @i
10. ≤loc(e1) ≤ ≤loc(e2)
⊢ map(λe.info(e);≤loc(e1)) ≤ map(λe.info(e);≤loc(e2))
BY
{ (MoveToConcl (-1)
   THEN (GenConcl ⌈≤loc(e1) = L1 ∈ (E List)⌉⋅ THENA Auto)
   THEN (GenConcl ⌈≤loc(e2) = L2 ∈ (E List)⌉⋅ THENA Auto)
   THEN All Thin
   THEN Auto) }

1
1. f : Name ─→ Type@i'
2. es : EO+(Message(f))@i'
3. L1 : E List@i
4. L2 : E List@i
5. L1 ≤ L2@i
⊢ map(λe.info(e);L1) ≤ map(λe.info(e);L2)

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type@i'
2.  [Info]  :  Type
3.  es  :  EO+(Message(f))@i'
4.  hdr  :  Name@i
5.  locs  :  bag(Id)@i
6.  hdr  encodes  Id  \mtimes{}  Info
7.  e1  :  E@i
8.  e2  :  E@i
9.  e1  \mleq{}loc  e2  @i
10.  \mleq{}loc(e1)  \mleq{}  \mleq{}loc(e2)
\mvdash{}  map(\mlambda{}e.info(e);\mleq{}loc(e1))  \mleq{}  map(\mlambda{}e.info(e);\mleq{}loc(e2))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}\mleq{}loc(e1)  =  L1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}\mleq{}loc(e2)  =  L2\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  Auto)

---

Home Index