---

Step * 1 of Lemma ranked-eo-info-le-before


1. [L] : Id ─→ (Top List)
2. [rk] : Top
3. [e] : E
⊢ map(λe.info(e);≤loc(e)) ~ firstn((snd(e)) + 1;L (fst(e)))
BY
{ (Unfold `es-le-before` 0
   THEN (RWO "map_append_sq" 0 THENA Auto)
   THEN (RWO "ranked-eo-info-before" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "ranked-eo-info" 0 THENA Auto)) }

1
1. [L] : Id ─→ (Top List)
2. [rk] : Top
3. [e] : E
⊢ firstn(snd(e);L (fst(e))) @ [L (fst(e))[snd(e)]] ~ firstn((snd(e)) + 1;L (fst(e)))

---

Latex:

---

Latex:

1.  [L]  :  Id  {}\mrightarrow{}  (Top  List)
2.  [rk]  :  Top
3.  [e]  :  E
\mvdash{}  map(\mlambda{}e.info(e);\mleq{}loc(e))  \msim{}  firstn((snd(e))  +  1;L  (fst(e)))


By

---

Latex:
(Unfold  `es-le-before`  0
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
  THEN  (RWO  "ranked-eo-info-before"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "ranked-eo-info"  0  THENA  Auto))

---

Home Index