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