OAI/Computability/BinPacking/Computation/Machine.lean

GitHub source file

98 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.encodeWords line 12
2. def OAI.BinPackingGames.Foundations.Complexity.decodeWordsAux line 16
3. def OAI.BinPackingGames.Foundations.Complexity.decodeWords line 22
4. theorem OAI.BinPackingGames.Foundations.Complexity.decodeWordsAux_word line 24
5. theorem OAI.BinPackingGames.Foundations.Complexity.decodeWords_encodeWords line 34
6. theorem OAI.BinPackingGames.Foundations.Complexity.encodeWords_injective line 42
7. theorem OAI.BinPackingGames.Foundations.Complexity.encodeWord_length line 47
8. theorem OAI.BinPackingGames.Foundations.Complexity.encodeWords_append line 50
9. theorem OAI.BinPackingGames.Foundations.Complexity.encodeWords_length line 56
10. theorem OAI.BinPackingGames.Foundations.Complexity.encodeWords_length_le line 62
11. def OAI.BinPackingGames.Foundations.Complexity.literalWords line 76
12. def OAI.BinPackingGames.Foundations.Complexity.clauseWords line 79
13. def OAI.BinPackingGames.Foundations.Complexity.formulaWords line 82
14. def OAI.BinPackingGames.Foundations.Complexity.formulaBits line 85
15. theorem OAI.BinPackingGames.Foundations.Complexity.literalWords_length line 87
16. theorem OAI.BinPackingGames.Foundations.Complexity.clauseWords_length line 90
17. theorem OAI.BinPackingGames.Foundations.Complexity.clausesWords_length line 93
18. theorem OAI.BinPackingGames.Foundations.Complexity.formulaWords_length line 102
19. theorem OAI.BinPackingGames.Foundations.Complexity.literalBits_length_le line 107
20. theorem OAI.BinPackingGames.Foundations.Complexity.clauseBits_length_le line 111
21. theorem OAI.BinPackingGames.Foundations.Complexity.clausesBits_length_le line 119
22. theorem OAI.BinPackingGames.Foundations.Complexity.formulaBits_length_le line 129
23. def OAI.BinPackingGames.Foundations.Complexity.parseLiteral line 142
24. theorem OAI.BinPackingGames.Foundations.Complexity.parseLiteral_encoded line 151
25. def OAI.BinPackingGames.Foundations.Complexity.parseClause line 157
26. theorem OAI.BinPackingGames.Foundations.Complexity.clause_three_entries line 163
27. theorem OAI.BinPackingGames.Foundations.Complexity.parseClause_encoded line 170
28. def OAI.BinPackingGames.Foundations.Complexity.parseClauses line 175
29. theorem OAI.BinPackingGames.Foundations.Complexity.parseClauses_encoded line 182
30. def OAI.BinPackingGames.Foundations.Complexity.decodeFormulaWords line 189
31. theorem OAI.BinPackingGames.Foundations.Complexity.decodeFormulaWords_encoded line 195
32. def OAI.BinPackingGames.Foundations.Complexity.decodeFormulaBits line 203
33. theorem OAI.BinPackingGames.Foundations.Complexity.decodeFormulaBits_encoded line 206
34. theorem OAI.BinPackingGames.Foundations.Complexity.formulaBits_injective line 210
35. def OAI.BinPackingGames.Foundations.Complexity.parseLabel line 215
36. theorem OAI.BinPackingGames.Foundations.Complexity.parseLabel_value line 218
37. theorem OAI.BinPackingGames.Foundations.Complexity.parseLabels_values line 221
38. def OAI.BinPackingGames.Foundations.Complexity.parseImages line 227
39. theorem OAI.BinPackingGames.Foundations.Complexity.parseImages_values line 233
40. def OAI.BinPackingGames.Foundations.Complexity.findPreimage line 240
41. theorem OAI.BinPackingGames.Foundations.Complexity.findPreimage_permutation line 243
42. def OAI.BinPackingGames.Foundations.Complexity.searchedInverse line 262
43. theorem OAI.BinPackingGames.Foundations.Complexity.searchedInverse_permutation line 265
44. def OAI.BinPackingGames.Foundations.Complexity.tableWords line 271
45. def OAI.BinPackingGames.Foundations.Complexity.parsePermutation line 274
46. theorem OAI.BinPackingGames.Foundations.Complexity.parsePermutation_encoded line 283
47. theorem OAI.BinPackingGames.Foundations.Complexity.tableWords_length line 290
48. def OAI.BinPackingGames.Foundations.Complexity.constraintWords line 293
49. def OAI.BinPackingGames.Foundations.Complexity.parseConstraint line 296
50. theorem OAI.BinPackingGames.Foundations.Complexity.parseConstraint_encoded line 305
51. def OAI.BinPackingGames.Foundations.Complexity.parseConstraints line 314
52. theorem OAI.BinPackingGames.Foundations.Complexity.parseConstraints_encoded line 322
53. def OAI.BinPackingGames.Foundations.Complexity.gameWords line 331
54. def OAI.BinPackingGames.Foundations.Complexity.gameBits line 334
55. def OAI.BinPackingGames.Foundations.Complexity.decodeGameWords line 336
56. theorem OAI.BinPackingGames.Foundations.Complexity.decodeGameWords_encoded line 346
57. def OAI.BinPackingGames.Foundations.Complexity.decodeGameBits line 354
58. theorem OAI.BinPackingGames.Foundations.Complexity.decodeGameBits_encoded line 357
59. theorem OAI.BinPackingGames.Foundations.Complexity.gameBits_injective line 361
60. theorem OAI.BinPackingGames.Foundations.Complexity.constraintWords_length line 366
61. theorem OAI.BinPackingGames.Foundations.Complexity.constraintsWords_length line 369
62. theorem OAI.BinPackingGames.Foundations.Complexity.gameWords_length line 378
63. def OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.skipWord line 387
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.skipWord_encodeWord line 392
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.skipWord_iterate_encodeWords line 399
66. def OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.headWord line 410
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWord line 415
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWords line 423
69. def OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.lookupBits line 429
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.lookupBits_encodeWords line 432
71. def OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded line 437
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.decodeWords_encodeWord line 442
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_encode line 446
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_some line 451
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_none line 456
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.encoded_selected_split line 461
77. def OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.scannedBits line 473
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.encoded_prefix_length_le line 476
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.scannedBits_le line 485
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.scannedBits_of_some line 489
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.selected_scan_length_le line 496
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.output_length_le line 503
83. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.index_length_le line 510
84. def OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps line 521
85. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length_strong line 526
86. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length line 540
87. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_lt line 545
88. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_some line 560
89. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps_add_length_of_invalid line 566
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookupSpec.steps_le_input_encoding_size line 580
91. def OAI.BinPackingGames.Foundations.Complexity.naturalWordsEncoding line 590
92. def OAI.BinPackingGames.Foundations.Complexity.formulaEncoding line 595
93. def OAI.BinPackingGames.Foundations.Complexity.gameEncoding line 600
94. def OAI.BinPackingGames.Foundations.Complexity.prefixBitMachine line 605
95. def OAI.BinPackingGames.Foundations.Complexity.prefixBitPolyTime line 616
96. def OAI.BinPackingGames.Foundations.Complexity.enlargePolynomialBound line 635
97. def OAI.BinPackingGames.Foundations.Complexity.composeMachinePhases line 648
98. structure OAI.BinPackingGames.Foundations.Complexity.PolynomialGapReduction line 660