OAI/Computability/BinPacking/Computation/MachineRegularOwnerBodyBounds.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.joinTrace line 11
2. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.oneStep line 15
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataPlacement line 19
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTrace line 29
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_local line 46
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_fuel line 60
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_global line 67
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_output line 81
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.copyCountTrace line 95
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.copyFuelTrace line 111
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.guardZeroStep line 128
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.guardPositiveStep line 134
13. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.dummyBits line 143
14. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexData line 147
15. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopData line 154
16. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopFrame line 158
17. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.preSteps line 162
18. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopSteps line 166
19. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupCost line 173
20. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime line 179
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyPlacement line 185
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyResultPlacement line 194
23. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyExecution line 205
24. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familySteps line 211
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyTrace line 215
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.coreFrame_eq line 235
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexPlacement line 253
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexTrace line 268
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working_fuel line 292
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working_scratch line 295
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopPositiveStep line 298
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopZeroStep line 309
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.bumpStep line 314
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopPrefixTrace line 324
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.preparationTrace line 352
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupFrame line 361
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits_zero line 402
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroFrame line 409
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopFrame line 419
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroTrace line 430
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopTrace line 444
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.loopTrace line 458
43. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.ownerInTime line 473
44. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps line 505
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTrace line 508
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps_le line 514
47. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize line 525
48. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide line 528
49. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.rowPolynomial line 530
50. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.outputPolynomial line 533
51. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.corePolynomial line 536
52. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial line 541
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial_eval line 545
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummyTimeBound_le line 561
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide_le line 572
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerPrefix_length_le line 582
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.growingOutput_length_le line 590
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummySteps_le line 601
59. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.prePolynomial line 632
60. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopPolynomial line 635
61. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupPolynomial line 638
62. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.timePolynomial line 641
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.preSteps_le line 645
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopSteps_le line 664
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.allLoopSteps_le line 681
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupSteps_working line 692
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupCost_le line 702
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerTime_le line 739
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.totalSteps_le line 756
70. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerInTime line 761