OAI/Computability/BinPacking/Computation/FinalCNFRowPlan.lean

GitHub source file

99 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.Reference line 10
2. structure OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.LiteralTemplate line 15
3. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.ClauseTemplate line 20
4. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.queryLiteral line 22
5. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.auxiliaryLiteral line 25
6. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.tautologyTemplate line 28
7. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.chainTemplates line 31
8. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.blockTemplates line 44
9. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.templates line 47
10. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.literalAt line 50
11. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.templates_length line 54
12. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.templates_true line 57
13. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.templates_false line 60
14. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates line 63
15. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.literalTemplates_length line 66
16. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.literalWords line 71
17. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.clauseWords line 74
18. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.words line 77
19. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.words_length line 80
20. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.resolve line 89
21. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.resolve_query_value line 93
22. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.resolve_auxiliary_value line 97
23. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.instantiateLiteral line 105
24. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause line 108
25. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.splitLong_twelve line 112
26. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates line 127
27. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.instantiate_templates_of_acceptance line 141
28. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.instantiateClause_words line 148
29. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.words_eq_block line 152
30. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTemplate.block_words_length line 160
31. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.Label line 172
32. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.labelEquiv line 174
33. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.labelEquiv_val line 176
34. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.labelIndex line 181
35. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.labelBits line 183
36. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.labelBits_labelIndex line 185
37. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.labelIndex_labelBits line 188
38. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.leftHalf line 191
39. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.rightHalf line 194
40. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.relationAddress line 197
41. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.relationAddress_val line 200
42. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex line 205
43. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.patternRelationIndex_eq line 208
44. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.tableGraph line 211
45. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.tableGraph_tail line 215
46. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.tableGraph_reverse line 218
47. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.tableGraph_accepts line 221
48. abbrev OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.tableVerifier line 226
49. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.relation_lookup_eq_verifier_accepts line 229
50. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.pattern_lookup_eq_verifier_accepts line 234
51. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.verifier_accepts_eq_lookup line 239
52. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.buffer_lookup_eq_verifier_accepts line 244
53. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFPattern.pattern_buffer_lookup_eq_verifier_accepts line 251
54. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow line 265
55. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_tail line 269
56. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_reverseIndex line 272
57. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_relation line 275
58. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows line 278
59. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_get line 281
60. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_reverseAt line 285
61. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_acceptsAt line 292
62. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRows_valid line 299
63. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable line 307
64. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_vertices line 313
65. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_darts line 316
66. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_row line 319
67. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tail line 322
68. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_reverseIndex line 327
69. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_relation line 332
70. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericRow_words line 337
71. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_rowList line 340
72. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableWords line 346
73. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_tableBits line 352
74. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_tail line 356
75. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_reverse line 360
76. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_head line 365
77. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_semantics_accepts line 371
78. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headIndex line 376
79. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue line 380
80. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_headValue_tableGraph line 386
81. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFTableAdapter.genericTable_pattern_relation line 392
82. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue line 405
83. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.auxiliaryFlag line 409
84. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.tailFlag line 413
85. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.headFlag line 417
86. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.pattern_lt line 421
87. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.referenceOffset line 425
88. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan line 429
89. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_length line 438
90. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.literalPlan_bits line 441
91. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.patternLiteral line 469
92. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan line 474
93. def OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan line 478
94. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_length line 481
95. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_length line 492
96. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.encodeWords_flatMap line 500
97. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.patternPlan_bits line 506
98. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.referenceValue_eq_resolve line 537
99. theorem OAI.BinPackingGames.Foundations.Complexity.FinalCNFMachine.Program.rowPlan_bits line 563