OAI/Computability/BinPacking/CookLevin/ClashMachine.lean

GitHub source file

101 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens line 13
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_eq_flatMap_range line 17
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_eq_ofFn line 23
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_succ_first line 31
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_congr line 35
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_length_le line 43
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forTokens_length_eq line 54
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.closeOr line 63
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.nonemptyTokens line 65
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.clashPairTokens line 68
11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.clashRowTokens line 71
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.clashTokens line 74
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.validityTokens line 77
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.presenceTokens line 80
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens line 84
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.threshold_zero_iff line 87
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens_length line 90
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens_succ line 97
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.selectorLoopTokens_presence line 110
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.presenceTokens_length line 118
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.exprTokens_disjoin line 127
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.forestTokens_ofFn line 135
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.muxTokens line 139
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.exprTokens_mux line 142
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.nonemptyTokens_eq line 147
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.clashPairTokens_eq line 152
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.clashRowTokens_eq line 159
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.clashTokens_eq line 169
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.validityTokens_eq line 178
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.presenceTokens_eq line 183
31. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.payloadSymbolTokens line 192
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.payloadSymbolTokens_eq line 196
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.inputCellTokens line 201
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.inputCellTokens_eq line 210
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initialCellTokens line 229
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initialCellTokens_eq line 238
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initTokens line 248
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initTokens_eq line 254
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initTokens_length_le line 262
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.validityTokens_length_le line 270
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody line 283
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_index line 288
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_label line 296
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_state line 303
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.configurationBody_cell line 310
46. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens line 319
47. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.tokenBound line 323
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_eq line 327
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_length line 342
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initialization_inputBits line 346
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_length_le line 352
52. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initializationTokens_compile line 362
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initialization_tokenWords_bounded line 371
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.InitializationTemplate.initialization_tokenBits_length_le line 377
55. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Alphabet line 404
56. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.State line 405
57. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.clean line 407
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.emitted line 409
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.emitted_output line 413
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.emitted_count line 418
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.emitted_other line 422
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.tokenBits_append line 426
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.emitted_append line 430
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.emitted_nil line 446
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.chain line 450
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.literal line 454
67. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.stepAux_literal line 460
68. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Input.Label line 469
69. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Input.(instance at line 473) line 473
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Input.statement line 481
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Input.steps line 492
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Input.identity_output line 494
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Input.trace line 501
74. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.leftMap line 550
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.rightMap line 551
76. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.inputLeftMap line 552
77. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.inputRightMap line 553
78. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.Label line 555
79. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.choose line 564
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.stepAux_choose line 569
81. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.statement line 574
82. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.offSteps line 591
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.offTrace line 593
84. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.steps line 634
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.trace line 638
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Pair.steps_le line 698
87. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.pairMap line 708
88. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.Label line 710
89. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.statement line 716
90. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.frame line 723
91. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.frame_current line 726
92. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.frame_remaining line 729
93. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.counter_frame line 732
94. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.emitted_frame line 740
95. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.increment_frame line 754
96. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.tokens line 759
97. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.tokens_zero line 762
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.tokens_succ line 764
99. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.steps line 773
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.trace line 777
101. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ClashMachine.Row.steps_le line 834