OAI/Computability/BinPacking/Computation/GraphCounterStart.lean

GitHub source file

104 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.bitLength line 10
2. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.bitLength_zero line 12
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.bitLength_positive line 14
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.bitLength_half line 17
5. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.increments line 24
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.increments_true line 27
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.increments_half line 30
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.increments_false line 34
9. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.coreTime line 39
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.coreTime_zero line 44
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.coreTime_positive line 46
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.coreTime_bound line 50
13. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.Alphabet line 60
14. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.State line 61
15. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.initialState line 63
16. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.rawTapes line 65
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.update_input line 70
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.update_scratch line 75
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.update_output line 80
20. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.stripLoop line 85
21. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.guardLoop line 91
22. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.halfLoop line 100
23. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.program line 109
24. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.machine line 116
25. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.configuration line 127
26. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.next line 131
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.stripStep_true line 133
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.stripStep_false line 141
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.stripTrace line 149
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.halfStep_nil line 165
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.halfStep_false line 173
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.halfStep_true line 182
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.halfTrace line 191
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.restoreTrace line 223
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.guardStep_zero line 240
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.guardStep_positive line 248
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.coreTrace line 260
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.initList_eq line 292
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.haltList_eq line 300
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.initialStep line 308
41. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.totalTime line 317
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.totalTime_bound line 319
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.machineTrace line 324
44. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.outputsInTime line 339
45. def OAI.BinPackingGames.Foundations.Complexity.MachineLogCounter.computableInPolyTime line 345
46. inductive OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraTape line 372
47. abbrev OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList line 376
48. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_getElem?_ctorIdx_eq line 378
49. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraTape.enumList_nodup line 382
50. instance OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.(instance at line 384) line 384
51. inductive OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraLabel line 388
52. abbrev OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList line 393
53. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_getElem?_ctorIdx_eq line 396
54. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.ExtraLabel.enumList_nodup line 400
55. instance OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.(instance at line 402) line 402
56. abbrev OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.Tape line 406
57. abbrev OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.Label line 407
58. abbrev OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.Alphabet line 408
59. abbrev OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.State line 409
60. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.initialState line 411
61. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockLabel line 413
62. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockStatement line 417
63. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.readHeader line 427
64. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.program line 433
65. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.machine line 451
66. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockTapes line 462
67. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockConfiguration line 466
68. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockTapes_update line 470
69. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockStatement_simulation line 477
70. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockStep line 502
71. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockInTime line 517
72. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.rounds line 532
73. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.rounds_le line 534
74. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.two_pow_rounds_le line 537
75. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.growth_pow_rounds_le line 544
76. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.sizeEnvelope line 552
77. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.semanticSize_geometric line 554
78. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.semanticSize_bound line 568
79. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial line 581
80. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.sizePolynomial_eval line 584
81. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.timePolynomial line 588
82. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.timePolynomial_eval line 593
83. abbrev OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.Alphabet line 601
84. abbrev OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.State line 602
85. abbrev OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.Labels line 603
86. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.program line 605
87. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.program_guard line 613
88. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.machine line 618
89. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.haltedConfiguration line 631
90. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.haltStep line 636
91. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.iterationTrace line 646
92. theorem OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.bodyCosts_bound line 662
93. def OAI.BinPackingGames.Foundations.Complexity.PCPIterationMachine.iterationInTime line 679
94. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.startExtra line 714
95. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.startMemory line 719
96. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.startMemory_input_update line 723
97. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.startMemory_sum_update line 731
98. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.headerStep_zero line 739
99. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.headerStep_succ line 753
100. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.headerTrace line 770
101. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.headerInTime line 787
102. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.initialMemory line 799
103. theorem OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.clockInitialMemory line 809
104. def OAI.BinPackingGames.Foundations.Complexity.GraphCounterModel.startInTime line 821