= Solution
Record the outcome at the first completed board and otherwise branch over every available move:
``
data Outcome = Winner Player | Draw deriving (Eq,Ord,Show)
finals :: Board -> [(Board,Outcome)]
finals b@(os,xs,es)
| won os = [(b,Winner O)]
| won xs = [(b,Winner X)]
| null es = [(b,Draw)]
| otherwise = concatMap (\q -> finals (play b q)) es
``
The <recursion> terminates because each recursive call decreases the number of empty positions by one. For correctness, induct on that number. A completed board contributes exactly its own outcome. Otherwise every legal continuation has a unique first available move, and the induction hypothesis covers exactly all completions after that move. <List concatenation> collects these branches without extending completed games. Repeated final positions are allowed here because the computation deliberately explores every legal move sequence.
Back to article page
