OAI/Combinatorics/IndependentSets/Machines/MachineRegularOwnerBodyBounds.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize line 13
  2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide line 16
  3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.rowPolynomial line 18
  4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.outputPolynomial line 21
  5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.corePolynomial line 24
  6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial line 29
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial_eval line 33
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummyTimeBound_le line 49
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide_le line 60
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerPrefix_length_le line 70
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.growingOutput_length_le line 78
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummySteps_le line 89
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.prePolynomial line 120
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopPolynomial line 123
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupPolynomial line 126
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.timePolynomial line 129
  17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.preSteps_le line 133
  18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopSteps_le line 152
  19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.allLoopSteps_le line 169
  20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupSteps_working line 180
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupCost_le line 190
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerTime_le line 227
  23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.totalSteps_le line 244
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerInTime line 249