OAI/Combinatorics/IndependentSets/Machines/PoweringRuntimeBudget.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.IndependentSetsGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_of_executionline 10 - theorem
OAI.IndependentSetsGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_from_inputline 20 - abbrev
OAI.IndependentSetsGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCountline 28 - theorem
OAI.IndependentSetsGames.Foundations.Complexity.PoweringRuntimeBudget.finish_steps_le_of_executionline 31 - theorem
OAI.IndependentSetsGames.Foundations.Complexity.PoweringRuntimeBudget.total_steps_le_of_executionline 46