OAI/Computability/MinUncut/PCP/Gap.lean

GitHub source file

76 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Hastad.SourceGap.ClauseGap line 14
2. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.third_pos line 19
3. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.third_le_one line 21
4. def OAI.MinUncutGames.Foundations.Hastad.SourceGap.repetitionCount line 23
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.repetitionCount_pos line 27
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.repeated_game_bound line 32
7. def OAI.MinUncutGames.Foundations.Hastad.SourceGap.source line 48
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.source_complete line 52
9. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.source_sound line 65
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.source_size line 76
11. def OAI.MinUncutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator line 87
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_ge_two line 89
13. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_pos line 93
14. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_pos line 96
15. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le_half line 101
16. theorem OAI.MinUncutGames.Foundations.Hastad.SourceNoiseParameter.noiseDenominator_inv_le line 107
17. def OAI.MinUncutGames.Foundations.Hastad.SourceGap.forError line 130
18. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.forError_complete line 134
19. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.forError_sound line 143
20. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGap.forError_size line 152
21. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorContract.NonemptyFormula line 164
22. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorContract.inputEncoding line 166
23. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorContract.sourceMap line 168
24. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorContract.errorMap line 172
25. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorContract.inputEncoding_mk line 176
26. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.Tape line 186
27. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.currentAt line 190
28. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.remainingAt line 193
29. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits line 196
30. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc line 204
31. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit line 207
32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_zero line 211
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_extra line 217
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_self line 221
35. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_setAcc line 225
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setAcc_apply line 229
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_setAcc line 232
38. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit_extra line 238
39. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.putDigit_setAcc line 242
40. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_putDigit line 249
41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc line 269
42. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.setDigits_snoc_base line 305
43. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.allBits line 311
44. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix line 314
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_eq_ofFn line 318
46. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.blocks line 327
47. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.blockPrefix_all line 330
48. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.configuration line 337
49. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.BodyTrace line 340
50. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.val_snoc line 351
51. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.zeros_snoc line 357
52. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.initialConfiguration line 362
53. def OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.finalConfiguration line 366
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.exists_schedule line 372
55. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.traversalInTime line 504
56. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.initial_current line 526
57. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.initial_remaining line 532
58. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.final_current line 537
59. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.final_remaining line 543
60. theorem OAI.MinUncutGames.Foundations.Hastad.SourceOdometerSchedule.final_accumulator line 549
61. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.Tape line 564
62. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.Ambient line 565
63. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.State line 566
64. inductive OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.Label line 571
65. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.bodyEntry line 580
66. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.next line 582
67. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.sourceStateEquiv line 585
68. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.program line 591
69. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.main line 608
70. def OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.machine line 610
71. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.finite_work_alphabets line 621
72. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.atCheck line 626
73. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGeneratorProgram.atReset line 630
74. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.source_initial line 645
75. theorem OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.initial_configuration line 649
76. def OAI.MinUncutGames.Foundations.Hastad.SourceGenerator.startupInTime line 662