Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Functional programming, design and analysis of algorithms / 3 / e

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.