OAI/Combinatorics/IndependentSets/Machines/MachineRegularExecutionBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_mono line 12
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial line 19
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial_eval line 27
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.internal_steps_le line 36
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.familyPolynomial line 55
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.family_budget_le line 59
  7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial line 71
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial_eval line 75
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.actual_row_bound_le line 81
  10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial line 88
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_add_output line 91
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularExecutionBounds.block_core_bound_le line 97
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide line 132
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.rowPolynomial line 133
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.outputPolynomial line 135
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.corePolynomial line 137
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial line 141
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupPolynomial line 144
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.timePolynomial line 145
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.bodySize line 149
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial_eval line 152
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalTimeBound_le line 167
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide_le line 178
  24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.vertexSteps_le line 188
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.clearSteps_frame line 214
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupSteps_le line 221
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.totalSteps_le line 252
  28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalInTime line 270