OAI/Computability/BinPacking/CookLevin/BoundedExecution.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.absorbingNext line 10
  2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.absorbingNext_of_none line 12
  3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.absorbingNext_of_some line 15
  4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.advance line 18
  5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.advance_iterate_none line 20
  6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.absorbing_of_successfulTrace line 23
  7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.executionToAbsorbing line 41
  8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.absorbing_eq_of_execution line 63
  9. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.stickyNext line 76
  10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run line 78
  11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run_zero line 81
  12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run_succ line 84
  13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.step_none_iff line 88
  14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.stickyNext_live line 95
  15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run_eq_halt_of_outputs line 104
  16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.outputs_of_run_eq_halt line 110
  17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.outputs_iff_run_eq_halt line 121
  18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.IsStickyTrace line 128
  19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.boundedTrace line 131
  20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.boundedTrace_isSticky line 134
  21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.trace_eq_run line 139
  22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.outputs_iff_trace line 155
  23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.stackCapacity line 170
  24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run_stack_bound line 174
  25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run_stack_le line 182
  26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.statement_budget line 188
  27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.StackBound line 202
  28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe line 205
  29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.stackBound line 218
  30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.push_room line 223
  31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.mono line 227
  32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.StatementSafe.resultBound line 248
  33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.stackBound_of_budget line 268
  34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.statementSafe_of_budget line 275
  35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.run_statement_safe line 335
  36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.trace_stack_le line 341
  37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.BoundedExecution.trace_statement_safe line 348