OAI/Computability/DirectedFeedback/Games/GeneratorModel.lean

GitHub source file

105 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.Extra line 11
2. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.Tape line 12
3. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.State line 13
4. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.outputTape line 15
5. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.accumulatorTape line 16
6. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.headerControl line 18
7. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.headerSlots line 36
8. abbrev OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.ControlAmbient line 52
9. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.controlStateEquiv line 54
10. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.initialQuery line 63
11. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.initialState line 66
12. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.initialAmbient line 69
13. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.control_initial line 72
14. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.coefficientKeys line 75
15. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.mem_coefficientKeys line 83
16. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.workKeys line 89
17. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.mem_workKeys line 95
18. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.allTapes line 105
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.mem_allTapes line 113
20. def OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.clearKeys line 133
21. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.mem_clearKeys line 138
22. theorem OAI.DFVSGames.Foundations.Hastad.SourceGeneratorModel.accumulator_ne_output line 143
23. structure OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.Layout line 155
24. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.statement line 165
25. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.resultTapes line 170
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.result_bits line 174
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.result_count line 178
28. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.result_accumulator line 182
29. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.result_frame line 187
30. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.trace line 192
31. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.inTime line 238
32. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.inTime_steps line 252
33. def OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.machine line 261
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceHeaderAccumulate.source_inputBits_header line 272
35. abbrev OAI.DFVSGames.Foundations.Hastad.SourceStartup.Tape line 291
36. abbrev OAI.DFVSGames.Foundations.Hastad.SourceStartup.State line 292
37. abbrev OAI.DFVSGames.Foundations.Hastad.SourceStartup.ArithmeticLabel line 293
38. abbrev OAI.DFVSGames.Foundations.Hastad.SourceStartup.Label line 294
39. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.headerLayout line 299
40. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.arithmeticEntry line 307
41. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.arithmeticProgram line 310
42. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.program line 315
43. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialTapes line 321
44. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.initializedTapes line 324
45. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.countedTapes line 327
46. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.outputTapes line 331
47. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.readyTapes line 336
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_formula line 343
49. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_current line 347
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_remaining line 351
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_variableHeader line 355
52. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_clauseHeader line 361
53. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_work line 367
54. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_work_raw line 374
55. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_field line 378
56. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialized_clean line 385
57. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.initialArithmeticMetadata line 399
58. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initial_arithmetic line 402
59. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.initial_loader line 406
60. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.initializeInTime line 410
61. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.arithmeticInTime line 426
62. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.arithmeticConfiguration line 448
63. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.arithmetic_step line 454
64. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.arithmeticPlacedInTime line 472
65. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.phaseBound line 487
66. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.phasesInTime line 493
67. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.output_eq_ready line 502
68. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_formula line 526
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_current line 529
70. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_remaining line 532
71. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_variableHeader line 535
72. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_clauseHeader line 538
73. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_leftBlock line 541
74. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_dummy line 545
75. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_accumulator line 549
76. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_field line 553
77. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_work_blank line 556
78. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_sharedWork line 562
79. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.ready_sharedFrame line 566
80. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.startupInTime line 576
81. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.timePolynomial line 584
82. theorem OAI.DFVSGames.Foundations.Hastad.SourceStartup.phaseBound_le_polynomial line 589
83. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.startupInPolynomialTime line 610
84. def OAI.DFVSGames.Foundations.Hastad.SourceStartup.machine line 619
85. inductive OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.Label line 641
86. abbrev OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.Layout line 647
87. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.digits line 649
88. theorem OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.horner_value line 652
89. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.steps line 656
90. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.operandLength line 659
91. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.timePolynomial line 662
92. theorem OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.timePolynomial_eval line 666
93. theorem OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.steps_le_timePolynomial line 671
94. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.statement line 688
95. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.program line 696
96. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.coefficientTapes line 700
97. theorem OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.affineTrace line 703
98. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.affineInTime line 771
99. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.affineInPolynomialTime line 788
100. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.programInTime line 805
101. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.leftBaseInTime line 817
102. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.rightBaseInTime line 836
103. theorem OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.resultTapes_dummy line 858
104. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.machine line 863
105. def OAI.DFVSGames.Foundations.Hastad.SourceBasePhase.machineInTime line 874