OAI/Computability/DirectedFeedback/Encoding/Bounds.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.formulaBits_length line 12
2. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_variables line 20
3. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_clauses line 25
4. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.formulaBits_length_ge_two line 30
5. def OAI.DFVSGames.Foundations.Hastad.SourceBounds.bitCountFormula line 35
6. def OAI.DFVSGames.Foundations.Hastad.SourceBounds.bitCoefficient line 38
7. def OAI.DFVSGames.Foundations.Hastad.SourceBounds.testCoefficient line 40
8. def OAI.DFVSGames.Foundations.Hastad.SourceBounds.occurrenceCoefficient line 43
9. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.one_le_input_power line 45
10. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.bitCountFormula_le_input line 51
11. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.testCountFormula_le_input line 66
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.testCountFormula_add_one_le_input line 76
13. def OAI.DFVSGames.Foundations.Hastad.SourceBounds.sourceSizeBound line 85
14. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.sourceBits_length_le line 88
15. def OAI.DFVSGames.Foundations.Hastad.SourceBounds.sourcePolynomial line 98
16. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.sourcePolynomial_eval line 103
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.card_testTape line 110
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.testTapeEncoding_size line 115
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.card_sourceIndex line 119
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.nBits_le_input line 126
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.rawSourceList_length_eq line 131
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.rawSourceList_length_le_input line 137
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.sourceList_length_le_input line 144
24. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.sourceInput_bits_polynomial line 154
25. theorem OAI.DFVSGames.Foundations.Hastad.SourceBounds.fixed_parameters_source_size line 162
26. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.Profile line 175
27. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.equalityProfile line 177
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.equalityProfile_encodeWord line 180
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.statement_roundtrip line 195
30. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.copyStateEquiv line 200
31. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.normalState line 207
32. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.copyStatement line 209
33. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.copyInCompareState line 214
34. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.nonDestructiveCompareInTime line 261
35. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.setEntry line 319
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.setEntry_apply line 322
37. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.setExpected line 328
38. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.foldProfile line 332
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.foldProfile_apply line 335
40. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.Tape line 351
41. abbrev OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.Label line 352
42. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.labelAt line 354
43. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.storePair line 357
44. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.profileProgram line 362
45. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.pairTime line 382
46. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.prefixProfile line 386
47. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.prefixTime line 390
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.prefixProfile_succ line 394
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.prefixTime_succ line 402
50. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.stageInTime line 409
51. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.prefixInTime line 454
52. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.allPairs line 474
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.mem_allPairs line 477
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.length_allPairs line 480
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.foldProfile_allPairs line 483
56. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.profileMachine line 488
57. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.profileInTime line 499
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.pairTime_le line 525
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.totalTime_le line 534
60. def OAI.DFVSGames.Foundations.Complexity.MachineFieldProfile.profileInTime_bounded line 544
61. def OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.positionEncoding line 566
62. def OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.names line 569
63. def OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.nameWords line 573
64. def OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.reindexProfile line 577
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.computed_profile_eq line 581
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.prepared_signature_eq line 589
67. theorem OAI.DFVSGames.Foundations.Hastad.SourceProfileBridge.nameWords_length_le_input line 597
68. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.positions line 614
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.mem_positions line 617
70. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.fillSigns line 620
71. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.fillSigns_apply line 624
72. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.fillSigns_positions line 638
73. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.State line 647
74. abbrev OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.Alphabet line 648
75. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.finish line 650
76. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.peekChain line 655
77. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.statement line 663
78. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.readSigns line 667
79. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.stepAux_peekChain line 670
80. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.stepAux_statement line 683
81. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.peekChain_pushBound line 690
82. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.statement_pushBound line 698
83. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.readSigns_of_unary line 703
84. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.loadStep line 711
85. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.loadInTime line 722
86. theorem OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.loaded_ofContext line 740
87. def OAI.DFVSGames.Foundations.Hastad.SourceSignLoad.loadContextInTime line 752