OAI/Combinatorics/IndependentSets/Machines/PoweringMachineRuntime.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish line 15
  2. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration line 19
  3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget line 23
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_ready line 27
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_output line 35
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_vertices line 46
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_darts line 54
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.serialized_eq line 63
  9. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishExecution line 70
  10. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps line 91
  11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.finishExecution line 95
  12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.execution line 120
  13. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps_le line 132
  14. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.execution_budget_le line 143
  15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime line 152
  16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime_finite_alphabet line 172