# Gale-Stewart Games

 Title: Gale-Stewart Games Author: Sebastiaan Joosten Submission date: 2021-04-23 Abstract: This is a formalisation of the main result of Gale and Stewart from 1953, showing that closed finite games are determined. This property is now known as the Gale Stewart Theorem. While the original paper shows some additional theorems as well, we only formalize this main result, but do so in a somewhat general way. We formalize games of a fixed arbitrary length, including infinite length, using co-inductive lists, and show that defensive strategies exist unless the other player is winning. For closed games, defensive strategies are winning for the closed player, proving that such games are determined. For finite games, which are a special case in our formalisation, all games are closed. BibTeX: @article{GaleStewart_Games-AFP, author = {Sebastiaan Joosten}, title = {Gale-Stewart Games}, journal = {Archive of Formal Proofs}, month = apr, year = 2021, note = {\url{https://isa-afp.org/entries/GaleStewart_Games.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Parity_Game Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.