---

Step * of Lemma ranked-eo-info-before

∀[L:Id ⟶ (Top List)]. ∀[rk:Top]. ∀[e:E].  (map(λe.info(e);before(e)) ~ firstn(snd(e);L (fst(e))))
BY
{ (Intros
   THEN RWW "ranked-eo-E-sq" 0
   THEN Auto
   THEN (RWO "ranked-eo-before" 0 THENA Auto)
   THEN (RWO "ranked-eo-info" 0 THENA Auto)
   THEN (RWO "map-map" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN (RWO "firstn_map_upto" 0 THENA Auto)
   THEN RepeatFor 2 ((EqCD THEN Auto))) }

1
.....subterm..... T:t
1:n
1. L : Id ⟶ (Top List)
2. rk : Top
3. e : E
⊢ (snd(e)) = imin(||L (fst(e))||;snd(e)) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[L:Id  {}\mrightarrow{}  (Top  List)].  \mforall{}[rk:Top].  \mforall{}[e:E].    (map(\mlambda{}e.info(e);before(e))  \msim{}  firstn(snd(e);L  (fst(e))))


By

---

Latex:
(Intros
  THEN  RWW  "ranked-eo-E-sq"  0
  THEN  Auto
  THEN  (RWO  "ranked-eo-before"  0  THENA  Auto)
  THEN  (RWO  "ranked-eo-info"  0  THENA  Auto)
  THEN  (RWO  "map-map"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  (RWO  "firstn\_map\_upto"  0  THENA  Auto)
  THEN  RepeatFor  2  ((EqCD  THEN  Auto)))

---

Home Index