OAI/Computability/BinPacking/PCP/RawInitialMachineBudget.lean

GitHub source file

110 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.Label line 13
2. abbrev OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.RelationTable line 14
3. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationIndex line 18
4. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationIndex_val line 20
5. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationAt line 23
6. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationOf line 26
7. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationAt_relationOf line 29
8. structure OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.DartRow line 33
9. abbrev OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.Rows line 38
10. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.reverseAt line 40
11. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.acceptsAt line 43
12. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.Valid line 46
13. instance OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.(instance at line 50) line 50
14. structure OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.Table line 54
15. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowList line 60
16. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowList_length line 62
17. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics line 65
18. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_reverse line 76
19. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_tail line 79
20. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_accepts line 82
21. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.graphRows line 85
22. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.reverseAt_graphRows line 88
23. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.acceptsAt_graphRows line 93
24. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.graphRows_valid line 98
25. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.ofGraph line 106
26. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_reverse line 109
27. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_tail line 114
28. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_accepts line 120
29. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_edgeSatisfied line 125
30. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.constraintGraph_ext line 130
31. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph line 144
32. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_rejectionCount line 153
33. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.enumeratedGraph line 159
34. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_edgeSatisfied line 175
35. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_rejectionCount line 183
36. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.ofEnumeratedGraph line 195
37. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.bitWord line 199
38. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseBit line 201
39. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseBit_bitWord line 206
40. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseBits_bitWords line 209
41. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationWords line 215
42. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationWords_length line 217
43. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseRelation line 220
44. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseRelation_encoded line 226
45. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowWords line 233
46. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseRow line 236
47. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseRow_encoded line 244
48. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseRows line 252
49. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.parseRows_encoded line 260
50. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.tableWords line 266
51. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.tableBits line 269
52. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.decodeTableWords line 271
53. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.decodeTableWords_encoded line 282
54. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.decodeTableBits line 290
55. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.decodeTableBits_encoded line 293
56. def OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.encoding line 297
57. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.tableBits_injective line 302
58. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowWords_length line 304
59. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowsWords_length line 310
60. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.tableWords_length line 316
61. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.tableWords_length_le_bits line 321
62. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.relationBits_length_le line 326
63. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowBits_length_le line 334
64. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.rowsBits_length_le line 343
65. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.tableBits_length_le line 353
66. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.vertices_le_tableBits_length line 362
67. theorem OAI.BinPackingGames.Foundations.PCP.GenericGraphTables.darts_le_tableBits_length line 368
68. def OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial line 381
69. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_eval line 384
70. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.encodingPolynomial_mono line 388
71. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.rowBound_le_polynomial line 394
72. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.generic_size_add_two_le_bits line 404
73. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_polynomial line 410
74. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.generic_bits_le_of_size_le line 416
75. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.size_add_two_le_bits line 421
76. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.bits_le_polynomial line 427
77. theorem OAI.BinPackingGames.Foundations.PCP.GraphTableComplexity.bits_le_of_size_le line 433
78. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.rowWidth line 458
79. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.rowOffset line 460
80. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.rowsWords_split line 462
81. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.rowsBits_split line 471
82. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.rowsBits_append_split line 480
83. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.prefixWords line 489
84. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.suffixWords line 492
85. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.prefixWords_length line 495
86. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_at_row line 500
87. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableBits_at_row line 509
88. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableBits_header line 515
89. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_row line 520
90. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_take_row line 527
91. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_tail line 533
92. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_reverse line 538
93. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_relation line 543
94. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.relationWords_get line 549
95. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_relation line 554
96. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_predicate line 564
97. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.rowOffset_lt_length line 571
98. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Input.relationOffset_lt_length line 579
99. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.nameSum line 595
100. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.bodyTime line 598
101. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.loopTime line 602
102. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.nameSum_le line 606
103. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.bodyTime_le line 613
104. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.loopTime_le line 620
105. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.input_header_bound line 642
106. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.graph_size_bound line 648
107. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.fullBudget line 655
108. def OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial line 659
109. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.timePolynomial_eval line 663
110. theorem OAI.BinPackingGames.Foundations.PCP.RawInitialMachineBudget.fullBudget_le line 667