Clopen determinacy with terminal losses (source code)

= Clopen determinacy with terminal losses

Allow terminal positions of an <infinite game of perfect information> to carry a losing-player label. A <clopen set> of infinite winning plays still gives a <determined infinite game>. At a position where all infinite continuations have one winner, the other player can win only by forcing a terminal loss for that winner. The usual <winning-position attractor in an infinite game> decides this reachability game. The tree of remaining undecided positions is <well-founded>: every infinite branch would eventually have its clopen payoff decided by a prefix. Assign the already decided winners upwards by <well-founded recursion>. Terminal labels are essential; a terminal node created by a covering need not be lost by the player whose turn would have come next.