---

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


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)
BY
{ (BLemma `iseg-map` THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Name  {}\mrightarrow{}  Type@i'
2.  es  :  EO+(Message(f))@i'
3.  L1  :  E  List@i
4.  L2  :  E  List@i
5.  L1  \mleq{}  L2@i
\mvdash{}  map(\mlambda{}e.info(e);L1)  \mleq{}  map(\mlambda{}e.info(e);L2)


By

---

Latex:
(BLemma  `iseg-map`  THEN  Auto)

---

Home Index