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.