OAI/Combinatorics/IndependentSets/Machines/MachineRegularOwnerBody.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.joinTrace line 13
  2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.oneStep line 17
  3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.metadataPlacement line 21
  4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTrace line 31
  5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_local line 48
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_fuel line 62
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_global line 69
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_output line 83
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.copyCountTrace line 97
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.copyFuelTrace line 113
  11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.guardZeroStep line 130
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.guardPositiveStep line 136
  13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.dummyBits line 145
  14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.vertexData line 149
  15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopData line 156
  16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopFrame line 160
  17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.preSteps line 164
  18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopSteps line 168
  19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupCost line 175
  20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime line 181
  21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.familyPlacement line 187
  22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.familyResultPlacement line 196
  23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.familyExecution line 207
  24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.familySteps line 213
  25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.familyTrace line 217
  26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.coreFrame_eq line 237
  27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.vertexPlacement line 255
  28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.vertexTrace line 270
  29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.working_fuel line 294
  30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.working_scratch line 297
  31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopPositiveStep line 300
  32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopZeroStep line 311
  33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.bumpStep line 316
  34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopPrefixTrace line 326
  35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.preparationTrace line 354
  36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupFrame line 363
  37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits_zero line 404
  38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroFrame line 411
  39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopFrame line 421
  40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroTrace line 432
  41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopTrace line 446
  42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.loopTrace line 460
  43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.ownerInTime line 475
  44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps line 507
  45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTrace line 510
  46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps_le line 516