OAI/Computability/DirectedFeedback/Machines/LoopInit.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.HeaderTape line 13
2. instance OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.(instance at line 16) line 16
3. abbrev OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.Tape line 20
4. inductive OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.Label line 22
5. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.variableHeader line 30
6. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.clauseHeader line 31
7. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.headerDestination line 32
8. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.readStart line 33
9. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.readLoop line 34
10. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.labelAt line 35
11. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.program line 37
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.atReadStart line 56
13. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.atReadLoop line 61
14. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.atReadDone line 66
15. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.copiedInput line 72
16. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.readOutput line 75
17. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.headerOutput line 79
18. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.clear_readOutput line 84
19. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.readOutput_work line 94
20. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.headerOutput_frame line 99
21. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.headerInTime line 103
22. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.digitOutput line 139
23. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.digitOutput_frame line 142
24. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.digitInTime line 146
25. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.stageTapes line 189
26. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.stageTapes_frame line 194
27. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.stageTapes_current line 205
28. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.stageTapes_remaining line 225
29. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.prefixInTime line 246
30. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.digitsInTime line 274
31. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.outputTapes line 293
32. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.initializeInTime line 296
33. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_current line 328
34. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_remaining line 332
35. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_frame line 336
36. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_work line 342
37. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_variableHeader line 347
38. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_clauseHeader line 352
39. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_headers line 357
40. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.output_formula line 363
41. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.timePolynomial line 368
42. theorem OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.timePolynomial_eval line 371
43. def OAI.DFVSGames.Foundations.Hastad.SourceLoopInit.machine line 375
44. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.rank line 395
45. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.reverseDigits line 398
46. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.reverseDigits_apply line 401
47. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.horner_value_sum line 405
48. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.horner_reverse_eq_rank line 420
49. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.reverseSlots line 439
50. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.reverseSlots_control line 442
51. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.reverseSlots_digit line 445
52. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.clean_reverseSlots line 451
53. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.statement line 458
54. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.program line 463
55. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.rankTrace line 468
56. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.rankInTime line 487
57. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.rankInPolynomialTime line 504
58. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.variableRankInTime line 523
59. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.clauseRankInTime line 539
60. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.programInTime line 555
61. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.machine line 567
62. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.machineInTime line 578
63. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.clauseSlots line 593
64. def OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.variableSlots line 610
65. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.clauseSlots_control line 627
66. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.clauseSlots_digit line 630
67. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.variableSlots_control line 633
68. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.variableSlots_digit line 636
69. theorem OAI.DFVSGames.Foundations.Hastad.SourceRankPhase.selectedDigits_loaded line 640
70. inductive OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.BodyWork line 660
71. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.BodyExtra line 668
72. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.Arena line 669
73. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.QueryState line 670
74. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.ArithmeticState line 671
75. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.State line 672
76. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.QueryMetadata line 673
77. abbrev OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.ArithmeticMetadata line 675
78. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.workTape line 680
79. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.variableHeader line 681
80. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.clauseHeader line 682
81. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.canonicalSignature line 684
82. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.canonicalState line 687
83. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.queryStateEquiv line 691
84. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.arithmeticStateEquiv line 697
85. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.rankControls line 703
86. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.clauseRankSlots line 713
87. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.variableRankSlots line 716
88. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.baseSlots line 719
89. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.querySources line 741
90. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.queryLayout line 746
91. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.perSlotCleanup line 758
92. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.finalBaseCleanup line 759
93. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeModel.initializer_arena line 761