OAI/Computability/DirectedFeedback/Machines/MachineRegularOriginalBody.lean

GitHub source file

153 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.rotationWords_resizeTable line 56
2. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.familyRotor_eq_familyCloudTable line 62
3. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_dart line 71
4. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.padding_zero_of_cloudSize_zero line 76
5. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_dummy line 80
6. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.cloudSize_pos_of_paddedCloud line 88
7. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFamilyBridge.familyCloudWords_of_zero line 96
8. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.Tape line 116
9. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.Alphabet line 117
10. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.CoreState line 118
11. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.MetaState line 119
12. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.FamilyState line 120
13. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.State line 121
14. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.Data line 122
15. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable line 123
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive line 125
17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.readyState line 128
18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTape line 132
19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView line 136
20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyTape line 141
21. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyView line 145
22. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView line 150
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_left line 154
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_right line 157
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_left line 165
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_right line 168
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_left line 176
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_right line 178
29. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataStates line 184
30. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyStates line 190
31. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexStates line 191
32. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.Label line 194
33. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.entry line 201
34. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearTape line 203
35. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearEntry line 207
36. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearSource line 210
37. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSource line 213
38. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.program line 217
39. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.frame line 228
40. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame line 233
41. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.cfg line 236
42. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.initialData line 239
43. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData line 252
44. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyData line 255
45. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits line 260
46. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData line 263
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.joinTrace_inline_MachineRegularOriginalBody line 267
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataPlacement line 271
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTrace line 279
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyPlacement line 295
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyResultPlacement line 303
52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyExecution line 316
53. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familySteps line 321
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.familyTrace line 325
55. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearMemory line 342
56. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearSteps line 347
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.identityPlacement_inline_MachineRegularOriginalBody line 352
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.drainTrace line 355
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearPrefixTrace line 371
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearTrace line 386
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.clearFrame line 392
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame_eq line 410
63. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData_eq line 430
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexPlacement line 434
65. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps line 445
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.vertexTrace line 449
67. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps line 468
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.originalTrace line 473
69. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBody.originalExecution line 489
70. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape line 510
71. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.State line 511
72. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet line 512
73. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.sumDecidableEq_inline_MachineRegularOwnerCleanup line 514
74. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeDecidableEq line 525
75. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeBEq line 537
76. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeLawfulBEq line 540
77. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeFintype line 544
78. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.core line 551
79. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.localRank line 552
80. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.count line 553
81. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape line 554
82. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.rotor line 555
83. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding line 556
84. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.level line 557
85. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel line 558
86. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch line 559
87. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes line 561
88. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label line 563
89. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.entry line 569
90. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry line 571
91. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction line 574
92. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.afterAddition line 583
93. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes line 586
94. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps line 589
95. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_apply line 592
96. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_prefix line 599
97. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_empty line 604
98. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_other line 608
99. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_scratch line 613
100. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.drainSteps_eq line 619
101. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.additionTraceAt line 625
102. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.traceAt line 650
103. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerCleanup.executionAt line 670
104. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix line 693
105. def OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix line 696
106. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_zero line 699
107. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_all line 703
108. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_succ line 709
109. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_zero line 717
110. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_all line 721
111. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksSuffix_succ line 727
112. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRegularLoopWords.blocksPrefix_append_suffix line 734
113. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.Tape line 752
114. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.Alphabet line 753
115. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.State line 754
116. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.Data line 755
117. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.CoreState line 756
118. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.MetaState line 757
119. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.FamilyState line 758
120. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable line 759
121. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 761) line 761
122. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 762) line 762
123. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.core line 764
124. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.paddingTape line 765
125. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.levelTape line 766
126. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.dummyFuel line 767
127. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.scratch line 768
128. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.readyState line 770
129. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTape line 772
130. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView line 775
131. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyTape line 779
132. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyView line 782
133. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView line 786
134. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView_left line 790
135. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView_right line 793
136. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyView_left line 799
137. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyView_right line 802
138. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView_left line 808
139. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView_right line 810
140. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataStates line 816
141. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.familyStates line 822
142. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.vertexStates line 828
143. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.Label line 834
144. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.entry line 846
145. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.program line 848
146. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.working line 881
147. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.frame line 885
148. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.cfg line 887
149. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.initialData line 890
150. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.metadataData line 903
151. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.seededData line 906
152. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits line 909
153. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBody.finalData line 912