[Haskell-cafe] Re: Optimization problem

[Ross Paterson]

On Mon, Sep 18, 2006 at 12:23:11AM +0100, Ross Paterson wrote:
> To prove that (even for partial and infinite lists ps)
> 
> 	splitSeq ps = [(a, seconds a ps) | a <- nub ps]
> 
> [...] we can establish, by induction on the input list,
> 
> (1)	fst (splitSeq' s ps) =
> 		[(a, seconds a ps) | a <- nub ps, not (member a s)]
> (2)	member x s  =>
> 		get x s (snd (splitSeq' s ps)) = seconds x ps

Oops, nub ps should be nub (map fst ps) in each case.