OAI/Computability/MinUncut/PCP/HeaderAccumulate.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.Layout line 13
2. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.statement line 23
3. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.resultTapes line 28
4. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.result_bits line 32
5. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.result_count line 36
6. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.result_accumulator line 40
7. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.result_frame line 45
8. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.trace line 50
9. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.inTime line 96
10. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.inTime_steps line 110
11. def OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.machine line 119
12. theorem OAI.MinUncutGames.Foundations.Hastad.SourceHeaderAccumulate.source_inputBits_header line 130
13. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceStartup.Tape line 150
14. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceStartup.State line 151
15. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ArithmeticLabel line 152
16. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceStartup.Label line 153
17. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.headerLayout line 157
18. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.arithmeticEntry line 165
19. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.arithmeticProgram line 168
20. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.program line 173
21. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialTapes line 179
22. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initializedTapes line 182
23. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.countedTapes line 185
24. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.outputTapes line 189
25. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.readyTapes line 194
26. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_formula line 201
27. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_current line 205
28. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_remaining line 209
29. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_variableHeader line 213
30. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_clauseHeader line 219
31. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_work line 225
32. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_work_raw line 232
33. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_field line 236
34. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialized_clean line 243
35. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initialArithmeticMetadata line 257
36. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initial_arithmetic line 260
37. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initial_loader line 264
38. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.initializeInTime line 268
39. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.arithmeticInTime line 284
40. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.arithmeticConfiguration line 306
41. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.arithmetic_step line 312
42. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.arithmeticPlacedInTime line 330
43. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.phaseBound line 345
44. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.phasesInTime line 351
45. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.output_eq_ready line 360
46. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_formula line 378
47. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_current line 381
48. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_remaining line 384
49. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_variableHeader line 387
50. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_clauseHeader line 390
51. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_leftBlock line 393
52. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_dummy line 397
53. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_accumulator line 401
54. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_field line 405
55. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_work_blank line 408
56. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_sharedWork line 414
57. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.ready_sharedFrame line 418
58. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.startupInTime line 428
59. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.timePolynomial line 436
60. theorem OAI.MinUncutGames.Foundations.Hastad.SourceStartup.phaseBound_le_polynomial line 441
61. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.startupInPolynomialTime line 462
62. def OAI.MinUncutGames.Foundations.Hastad.SourceStartup.machine line 471
63. inductive OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.Label line 494
64. abbrev OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.Layout line 500
65. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.digits line 502
66. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.horner_value line 505
67. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.steps line 509
68. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.operandLength line 512
69. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.timePolynomial line 515
70. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.timePolynomial_eval line 519
71. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.steps_le_timePolynomial line 524
72. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.statement line 541
73. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.program line 549
74. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.coefficientTapes line 553
75. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.affineTrace line 556
76. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.affineInTime line 624
77. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.affineInPolynomialTime line 641
78. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.programInTime line 658
79. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.leftBaseInTime line 670
80. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.rightBaseInTime line 689
81. theorem OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.resultTapes_dummy line 711
82. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.machine line 716
83. def OAI.MinUncutGames.Foundations.Hastad.SourceBasePhase.machineInTime line 727