OAI/Computability/UniqueGames/Machines/MachineDrain.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual complete-stack cleanup, with an arbitrary continuation. Each symbol costs one transition and the empty-stack branch costs one final transition.

  1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.Alphabet line 17
  2. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drain line 19
  3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drainTrace line 26
  4. def OAI.UniqueGamesTheorem.Foundations.Complexity.MachineDrain.drainInTime line 47