---

Step * of Lemma select-rev-append

∀[T:Type]. ∀[L,bs:T List]. ∀[i:ℕ||L|| + ||bs||].
  (rev(L) + bs[i] = if i <z ||L|| then L[||L|| - 1 - i] else bs[i - ||L||] fi  ∈ T)
BY
{ ((InductionOnList THEN Reduce 0)
   THEN Auto
   THEN AutoSplit
   THEN (RWO "4" 0 THENA Auto')
   THEN AutoSplit
   THEN Try (Complete ((RWO "select_cons_tl" 0 THEN Auto)))
   THEN RWO "select_cons_hd" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L,bs:T  List].  \mforall{}[i:\mBbbN{}||L||  +  ||bs||].
    (rev(L)  +  bs[i]  =  if  i  <z  ||L||  then  L[||L||  -  1  -  i]  else  bs[i  -  ||L||]  fi  )


By

---

Latex:
((InductionOnList  THEN  Reduce  0)
  THEN  Auto
  THEN  AutoSplit
  THEN  (RWO  "4"  0  THENA  Auto')
  THEN  AutoSplit
  THEN  Try  (Complete  ((RWO  "select\_cons\_tl"  0  THEN  Auto)))
  THEN  RWO  "select\_cons\_hd"  0
  THEN  Auto)

---

Home Index