---

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


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||
5. n + 1 < ||L||
⊢ L[n] ~ hd(rev(firstn(n + 1;L)))
BY
{ ((InstLemma `firstn_decomp` [⌜Top⌝;⌜n + 1⌝;⌜L⌝]⋅ THENA Auto)⋅
   THEN RWO "-1<" 0
   THEN (RWO "reverse-append" 0 THENA Auto)
   THEN Reduce 0
   THEN EqCD
   THEN Auto) }

---

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.  n  +  1  <  ||L||
\mvdash{}  L[n]  \msim{}  hd(rev(firstn(n  +  1;L)))


By

---

Latex:
((InstLemma  `firstn\_decomp`  [\mkleeneopen{}Top\mkleeneclose{};\mkleeneopen{}n  +  1\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  RWO  "-1<"  0
  THEN  (RWO  "reverse-append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto)

---

Home Index