OAI/Computability/MinUncut/Machines/PoweringRuntimeBudget.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.MinUncutGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_of_executionline 11 - theorem
OAI.MinUncutGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_from_inputline 21 - abbrev
OAI.MinUncutGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCountline 29 - theorem
OAI.MinUncutGames.Foundations.Complexity.PoweringRuntimeBudget.finish_steps_le_of_executionline 32 - theorem
OAI.MinUncutGames.Foundations.Complexity.PoweringRuntimeBudget.total_steps_le_of_executionline 47