OAI/Computability/MinUncut/PCP/HeaderCounts.lean

GitHub source file

107 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.Label line 21
2. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.start line 23
3. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.inner line 24
4. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.finish line 25
5. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.word line 27
6. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices line 30
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.indices_nodup line 34
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.word_slot line 38
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.control_not_mem line 43
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.digit_mem line 49
11. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared line 54
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_control line 58
13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.prepared_digit line 64
14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.clear_result line 71
15. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.statement line 90
16. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.steps line 100
17. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.trace line 103
18. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Eval.inTime line 145
19. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.leftValue line 163
20. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.rightValue line 164
21. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.dummyValue line 165
22. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.bitValue line 166
23. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue line 167
24. inductive OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Kind line 170
25. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList line 174
26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_getElem?_ctorIdx_eq line 176
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Kind.enumList_nodup line 180
28. instance OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 182) line 182
29. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.polynomial line 186
30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.polynomial_left_eval line 192
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.polynomial_right_eval line 194
32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.polynomial_occurrences_eval line 196
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.bitValue_eq_nBits line 200
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.occurrenceValue_eq_length line 205
35. inductive OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Control line 216
36. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList line 221
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList_getElem?_ctorIdx_eq line 224
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Control.enumList_nodup line 228
39. instance OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.(instance at line 230) line 230
40. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Coefficients line 234
41. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Layout line 239
42. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.coefficientBlock line 241
43. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.inputControl line 248
44. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.outputControl line 251
45. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.controlSlots line 254
46. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.localSlots line 262
47. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.control line 281
48. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots line 283
49. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_radix line 287
50. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accA line 289
51. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_accB line 291
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_destination line 293
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_counter line 295
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_scratch line 297
55. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalSlots_digit line 299
56. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.control_eq_iff line 303
57. structure OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Clean line 307
58. inductive OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Label line 319
59. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalStart line 325
60. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.afterEval line 327
61. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.statement line 332
62. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.resultTapes line 353
63. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.steps line 360
64. structure OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.WorkClean line 365
65. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.Clean.work line 373
66. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.WorkClean.update_output line 377
67. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.evalPhaseTrace line 387
68. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.trace_trans line 408
69. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.trace line 412
70. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.timePolynomial line 516
71. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.steps_le_timePolynomial line 523
72. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.inTime line 544
73. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.inPolynomialTime line 559
74. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.formulaInTime line 575
75. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_frame line 590
76. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_left line 596
77. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_occurrences line 599
78. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_dummy line 602
79. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_bits line 605
80. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_variableCount line 608
81. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_clauseCount line 611
82. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.result_source_headers line 615
83. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.program line 624
84. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.machine line 628
85. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderCounts.afterInitializationInTime line 639
86. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.Extra line 673
87. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.Tape line 674
88. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.State line 675
89. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.outputTape line 677
90. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.accumulatorTape line 678
91. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.headerControl line 680
92. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.headerSlots line 698
93. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.ControlAmbient line 714
94. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.controlStateEquiv line 716
95. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.initialQuery line 725
96. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.initialState line 728
97. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.initialAmbient line 731
98. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.control_initial line 734
99. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.coefficientKeys line 737
100. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.mem_coefficientKeys line 745
101. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.workKeys line 751
102. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.mem_workKeys line 757
103. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.allTapes line 767
104. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.mem_allTapes line 775
105. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.clearKeys line 795
106. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.mem_clearKeys line 800
107. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorModel.accumulator_ne_output line 805