OAI/Computability/MinUncut/Machines/PoweringMachineRuntime.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish line 16
  2. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration line 20
  3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget line 24
  4. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_ready line 28
  5. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_output line 36
  6. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_vertices line 47
  7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_darts line 55
  8. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.serialized_eq line 64
  9. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishExecution line 71
  10. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps line 92
  11. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.finishExecution line 96
  12. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.execution line 122
  13. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps_le line 134
  14. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.execution_budget_le line 145
  15. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime line 154
  16. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime_finite_alphabet line 180