OAI/Computability/BinPacking/Information/SourceNonempty.lean

GitHub source file

131 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.formulaBits_length line 18
2. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 26
3. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 31
4. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 36
5. def OAI.BinPackingGames.Foundations.Hastad.SourceBounds.bitCountFormula line 41
6. def OAI.BinPackingGames.Foundations.Hastad.SourceBounds.bitCoefficient line 44
7. def OAI.BinPackingGames.Foundations.Hastad.SourceBounds.testCoefficient line 46
8. def OAI.BinPackingGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 49
9. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.one_le_input_power line 51
10. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 57
11. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 72
12. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 82
13. def OAI.BinPackingGames.Foundations.Hastad.SourceBounds.sourceSizeBound line 91
14. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.sourceBits_length_le line 94
15. def OAI.BinPackingGames.Foundations.Hastad.SourceBounds.sourcePolynomial line 104
16. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 109
17. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.card_testTape line 116
18. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 121
19. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.card_sourceIndex line 125
20. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.nBits_le_input line 132
21. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 137
22. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 143
23. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 150
24. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 160
25. theorem OAI.BinPackingGames.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 168
26. def OAI.BinPackingGames.Foundations.Hastad.SourceSoundness.leftTable line 181
27. def OAI.BinPackingGames.Foundations.Hastad.SourceSoundness.rightOracle line 185
28. theorem OAI.BinPackingGames.Foundations.Hastad.SourceSoundness.rightOracle_answer line 193
29. theorem OAI.BinPackingGames.Foundations.Hastad.SourceSoundness.leftTable_answer line 199
30. theorem OAI.BinPackingGames.Foundations.Hastad.SourceSoundness.sourceList_sound line 203
31. theorem OAI.BinPackingGames.Foundations.Hastad.SourceSoundness.sourceList_sound_rat line 221
32. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.Label line 247
33. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.start line 249
34. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.inner line 250
35. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.finish line 251
36. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.word line 253
37. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices line 256
38. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices_nodup line 260
39. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.word_slot line 264
40. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.control_not_mem line 269
41. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.digit_mem line 275
42. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared line 280
43. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_control line 284
44. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_digit line 290
45. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.clear_result line 297
46. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.statement line 316
47. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.steps line 326
48. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.trace line 329
49. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Eval.inTime line 371
50. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.leftValue line 389
51. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.rightValue line 390
52. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.dummyValue line 391
53. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.bitValue line 392
54. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue line 393
55. inductive OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Kind line 396
56. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList line 400
57. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_getElem?_ctorIdx_eq line 402
58. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_nodup line 406
59. instance OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 408) line 408
60. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.polynomial line 412
61. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.polynomial_left_eval line 418
62. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.polynomial_right_eval line 420
63. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.polynomial_occurrences_eval line 422
64. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.bitValue_eq_nBits line 426
65. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue_eq_length line 431
66. inductive OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Control line 442
67. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList line 447
68. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList_getElem?_ctorIdx_eq line 450
69. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList_nodup line 454
70. instance OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 456) line 456
71. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Coefficients line 460
72. abbrev OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Layout line 465
73. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.coefficientBlock line 467
74. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.inputControl line 474
75. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.outputControl line 477
76. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.controlSlots line 480
77. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.localSlots line 488
78. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.control line 507
79. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots line 509
80. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_radix line 513
81. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accA line 515
82. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accB line 517
83. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_destination line 519
84. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_counter line 521
85. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_scratch line 523
86. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_digit line 525
87. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.control_eq_iff line 529
88. structure OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Clean line 533
89. inductive OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Label line 545
90. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalStart line 551
91. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.afterEval line 553
92. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.statement line 558
93. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.resultTapes line 579
94. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.steps line 586
95. structure OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.WorkClean line 591
96. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.Clean.work line 599
97. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.WorkClean.update_output line 603
98. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.evalPhaseTrace line 613
99. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.trace_trans line 634
100. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.trace line 638
101. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.timePolynomial line 742
102. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.steps_le_timePolynomial line 749
103. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.inTime line 770
104. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.inPolynomialTime line 785
105. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.formulaInTime line 801
106. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_frame line 816
107. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_left line 822
108. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_occurrences line 825
109. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_dummy line 828
110. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_bits line 831
111. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_variableCount line 834
112. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_clauseCount line 837
113. theorem OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.result_source_headers line 841
114. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.program line 850
115. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.machine line 854
116. def OAI.BinPackingGames.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime line 865
117. def OAI.BinPackingGames.Foundations.Hastad.SourceGap.ClauseGap line 897
118. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.third_pos line 902
119. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.third_le_one line 904
120. def OAI.BinPackingGames.Foundations.Hastad.SourceGap.repetitionCount line 906
121. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.repetitionCount_pos line 910
122. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.repeated_game_bound line 915
123. def OAI.BinPackingGames.Foundations.Hastad.SourceGap.source line 931
124. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.source_complete line 935
125. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.source_sound line 948
126. theorem OAI.BinPackingGames.Foundations.Hastad.SourceGap.source_size line 959
127. theorem OAI.BinPackingGames.Foundations.Hastad.SourceNonempty.real_clause_gap_of_count line 972
128. theorem OAI.BinPackingGames.Foundations.Hastad.SourceNonempty.clauseGap_of_count line 986
129. theorem OAI.BinPackingGames.Foundations.Hastad.SourceNonempty.cnf_nonempty_of_nonempty_darts line 997
130. theorem OAI.BinPackingGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap line 1006
131. theorem OAI.BinPackingGames.Foundations.Hastad.SourceNonempty.cnf_clauseGap_unit line 1018