---

Step * of Lemma ranked-eo-before

∀[L:Id ⟶ (Top List)]. ∀[rk:Top]. ∀[e:E].  (before(e) ~ map(λn.<fst(e), n>;upto(snd(e))))
BY
{ (Intro
   THEN RWO "ranked-eo-E-sq" 0
   THEN Auto
   THEN D -1
   THEN Thin
   (-1)⋅
   THEN D -1
   THEN Reduce 0
   THEN (GenConcl ⌜e1 = n ∈ ℕ⌝⋅ THENA Auto)
   THEN All Thin
   THEN CompNatInd (-1)) }

1
1. L : Id ⟶ (Top List)
2. rk : Top
3. i : Id
4. n : ℕ
5. ∀n:ℕn. (before(<i, n>) ~ map(λn.<i, n>;upto(n)))
⊢ before(<i, n>) ~ map(λn.<i, n>;upto(n))

---

Latex:

---

Latex:
\mforall{}[L:Id  {}\mrightarrow{}  (Top  List)].  \mforall{}[rk:Top].  \mforall{}[e:E].    (before(e)  \msim{}  map(\mlambda{}n.<fst(e),  n>upto(snd(e))))


By

---

Latex:
(Intro
  THEN  RWO  "ranked-eo-E-sq"  0
  THEN  Auto
  THEN  D  -1
  THEN  Thin
  (-1)\mcdot{}
  THEN  D  -1
  THEN  Reduce  0
  THEN  (GenConcl  \mkleeneopen{}e1  =  n\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  CompNatInd  (-1))

---

Home Index