= Solution
Use <mathematical induction> on $n$, which is finite even when the <list> is infinite. At $n=0$, the left side is `[] ++ xs = xs`. For the successor step, an empty <list> gives `[]`; for `x:xs`, the defining equations and <list concatenation> give
``
take (n+1) (x:xs) ++ drop (n+1) (x:xs)
= (x : take n xs) ++ drop n xs
= x : (take n xs ++ drop n xs)
= x : xs
``
The last step applies the <induction hypothesis> to the tail. A <bottom value> tail is allowed: for a wholly undefined list and a positive count both sides are undefined. Thus the equality is observationally valid for finite and infinite <lists>; no evaluation of an infinite length is used.
Back to article page
