---

Step * 3 of Lemma select-front-as-reduce


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||
BY
{ (ParallelLast' THEN RWO "-1" 0 THEN (D 0 THENA Auto)) }

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

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  \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(n  +  1;L)))
\mvdash{}  \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  <  ||L||


By

---

Latex:
(ParallelLast'  THEN  RWO  "-1"  0  THEN  (D  0  THENA  Auto))

---

Home Index