---

Step * of Lemma select-front-as-reduce

∀[n:ℕ]. ∀[L:Top List].
  L[n] ~ hd(reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];L)) supposing n < ||L||
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∀L:Top List
                  (reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];L) ~ rev(firstn(n + 1;L))) BY
               (InductionOnList THEN Reduce 0))
   ) }

1
1. n : ℕ
⊢ [] ~ []

2
1. n : ℕ
2. u : Top
3. v : Top List
4. reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) ~ rev(firstn(n + 1;v))
⊢ if ||reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v)|| <z n + 1
then reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v) @ [u]
else tl(reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];v)) @ [u]
fi  ~ rev(firstn(n + 1;[u / v]))

3
1. n : ℕ
2. ∀L:Top List. (reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];L) ~ rev(firstn(n + 1;L)))
⊢ ∀[L:Top List]. L[n] ~ hd(reduce(λu,x. if ||x|| <z n + 1 then x @ [u] else tl(x) @ [u] fi ;[];L)) supposing n < ||L||

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[L:Top  List].
    L[n]  \msim{}  hd(reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];L))  supposing  n  <  ||\000CL||


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mforall{}L:Top  List
                                (reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];L)  \msim{}  rev(firstn\000C(n
                                +  1;L)))  BY
                          (InductionOnList  THEN  Reduce  0))
  )

---

Home Index