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


1. : ℕ
2. Top List
3. reduce(λu,x. if ||x|| <then [u] else tl(x) [u] fi ;[];L) rev(firstn(n 1;L))
4. n < ||L||
5. ¬1 < ||L||
⊢ L[n] hd(rev(firstn(n 1;L)))
BY
(RWO "firstn_all" THEN Try (Complete (Auto'))) }

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


Latex:


Latex:

1.  n  :  \mBbbN{}
2.  L  :  Top  List
3.  reduce(\mlambda{}u,x.  if  ||x||  <z  n  +  1  then  x  @  [u]  else  tl(x)  @  [u]  fi  ;[];L)  \msim{}  rev(firstn(n  +  1;L))
4.  n  <  ||L||
5.  \mneg{}n  +  1  <  ||L||
\mvdash{}  L[n]  \msim{}  hd(rev(firstn(n  +  1;L)))


By


Latex:
(RWO  "firstn\_all"  0  THEN  Try  (Complete  (Auto')))




Home Index