OAI/Computability/BinPacking/Computation/MachineRegularExecutionBounds.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Extra line 14
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList line 18
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_getElem?_ctorIdx_eq line 20
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Extra.enumList_nodup line 24
5. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.(instance at line 26) line 26
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Tape line 30
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Alphabet line 31
8. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.State line 32
9. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Label line 34
10. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.ownerTapes line 45
11. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankTape line 47
12. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixTape line 55
13. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudTape line 70
14. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.program line 84
15. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankView line 110
16. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixView line 121
17. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudView line 139
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankView_left line 153
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankView_right line 155
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixView_left line 161
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixView_right line 167
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudView_left line 173
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudView_right line 175
24. structure OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.Data line 181
25. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.frame line 194
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.frame_index line 209
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.frame_query_empty line 212
28. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cfg line 215
29. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudData line 219
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudTrace line 225
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.join_trace line 261
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.drainAt line 265
33. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixData line 275
34. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixSteps line 279
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.prefixTrace line 282
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.selected_owner line 334
37. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.ownerData line 342
38. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder line 345
39. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.ownerSteps line 348
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.ownerTrace line 352
41. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankQuery line 398
42. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.queryFrame line 400
43. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.querySteps line 404
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.queryTrace line 406
45. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankData line 443
46. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder line 447
47. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankSteps line 451
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankTrace line 457
49. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.originalMember line 520
50. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.originalData line 523
51. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.totalTime line 527
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.originalTrace line 531
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.encodeWords_drop_length_le line 552
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.ownerRemainder_length_le line 559
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.rankRemainder_length_le line 563
56. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.timePolynomial line 574
57. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.overhead line 578
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.overhead_le line 582
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.totalTime_le line 587
60. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.originalInTime line 637
61. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularMetadata.cloudInTime line 652
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_mono line 671
63. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial line 678
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial_eval line 686
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.internal_steps_le line 695
66. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.familyPolynomial line 714
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.family_budget_le line 718
68. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial line 730
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial_eval line 734
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.actual_row_bound_le line 740
71. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial line 747
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_add_output line 750
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularExecutionBounds.block_core_bound_le line 756