OAI/Computability/BinPacking/Computation/PoweringMasterState.lean

GitHub source file

119 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.Alphabet line 14
2. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guard line 16
3. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.counterTapes line 23
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_counter line 27
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.counterTapes_other line 32
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardPushBound line 38
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.stepAux_succ line 42
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.stepAux_zero line 50
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardStep_succ line 58
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardStep_zero line 70
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_succ line 82
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardTrace_zero line 95
13. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_succ line 107
14. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryCounter.guardInTime_zero line 122
15. def OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.guardConfiguration line 147
16. def OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.bodyConfiguration line 153
17. def OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.exitConfiguration line 158
18. def OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.BodyTraces line 163
19. def OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.totalSteps line 172
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.totalSteps_zero line 175
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.totalSteps_succ line 178
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.loopTrace line 183
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.totalSteps_le line 216
24. def OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.loopInTime line 227
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.baseFrame line 248
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.counterFrame line 259
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCountedLoop.loopTrace_framed line 270
28. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLookup.Alphabet line 297
29. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discard line 299
30. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.select line 306
31. inductive OAI.BinPackingGames.Foundations.Complexity.MachineLookup.Label line 313
32. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLookup.Label.enumList line 317
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.Label.enumList_getElem?_ctorIdx_eq line 320
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.Label.enumList_nodup line 324
35. instance OAI.BinPackingGames.Foundations.Complexity.MachineLookup.(instance at line 326) line 326
36. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.program line 330
37. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.tapes line 339
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.tapes_index line 344
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.tapes_source line 350
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.tapes_destination line 356
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.tapes_other line 361
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.update_index line 367
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.update_source line 381
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.update_destination line 392
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.fieldTapes_eq line 398
46. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.machine line 405
47. inductive OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape line 422
48. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList line 426
49. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_getElem?_ctorIdx_eq line 428
50. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape.enumList_nodup line 432
51. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 434) line 434
52. inductive OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel line 438
53. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList line 442
54. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_getElem?_ctorIdx_eq line 444
55. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel.enumList_nodup line 448
56. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 450) line 450
57. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet line 454
58. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.HeaderState line 455
59. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.pushTrue line 457
60. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.stepAux_pushTrue line 462
61. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.pushTrue_pushBound line 474
62. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.headerProgram line 482
63. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.headerMachine line 498
64. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.initialTapes line 509
65. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.scanTapes line 513
66. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.finalTapes line 519
67. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.scanConfiguration line 525
68. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration line 530
69. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.initializeStep line 534
70. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.scanStep_zero line 544
71. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.scanStep_succ line 555
72. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.scanTrace line 572
73. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.headerTrace line 589
74. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.headerInTime line 601
75. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.remainingRows line 610
76. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_top line 613
77. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_step line 616
78. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.rowBase line 623
79. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces line 627
80. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.vertexBodyTraces_to_counted line 640
81. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime line 653
82. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_output line 676
83. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.varyingRowBase line 682
84. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces line 686
85. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.varyingVertexBodyTraces_to_counted line 699
86. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime_varying line 712
87. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_varying_output line 735
88. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discard_update_twice line 751
89. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discardStep_delimiter line 760
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discardStep_true line 773
91. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discard_empty_step line 786
92. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discardTrace_update line 802
93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discardTrace line 825
94. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.discardInTime line 844
95. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.OtherRegisters line 866
96. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.Master line 867
97. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.CompareState line 868
98. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.RowState line 869
99. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.compareEquiv line 871
100. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.rowEquiv line 874
101. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.compareEquiv_apply line 880
102. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.compareEquiv_symm_apply line 884
103. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.rowEquiv_apply line 888
104. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.rowEquiv_symm_apply line 892
105. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.withBuffer line 896
106. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.clean line 899
107. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.equalityBit_clean line 901
108. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.rowEquiv_withBuffer line 904
109. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.compareEquiv_withBuffer line 907
110. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.clearBuffer line 910
111. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.clearBuffer_apply line 913
112. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.clearBuffer_withBuffer line 918
113. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.encodedBlockAt line 925
114. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.stepAux_encodedBlockAt line 930
115. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.step_encodedBlockAt line 943
116. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.rowAt line 955
117. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.step_rowAt_clean line 960
118. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.rowInTime line 977
119. def OAI.BinPackingGames.Foundations.Complexity.PoweringMasterState.headerInTime line 999