OAI/Computability/MinUncut/Machines/MachineExpanderRowFrames.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData line 10
2. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.rowData line 17
3. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.control0 line 25
4. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstRow line 26
5. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue line 27
6. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstPair line 28
7. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex line 29
8. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn line 30
9. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.control1 line 31
10. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondRow line 32
11. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue line 33
12. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondPair line 34
13. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex line 35
14. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn line 36
15. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.control2 line 37
16. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.query1 line 38
17. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.query2 line 39
18. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue line 40
19. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.tableLength line 41
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_eq_firstRow line 43
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_eq_secondRow line 46
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_div_degree line 49
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_mod_degree line 50
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_div_degree line 51
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_mod_degree line 52
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_eq_residue line 54
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_eq_residue line 58
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveFirst_residue_eq_control1 line 62
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveSecond_residue_eq_control2 line 68
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstSelected line 74
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondSelected line 78
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.evaluateRow_eq line 82
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue_eq_step_reverseIndex line 85
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.rows_le_tableLength line 92
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_le_tableLength line 96
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_le_tableLength line 100
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_le_tableLength line 104
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_le_tableLength line 107
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.inputVertex_le_tableLength line 110
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex_le_tableLength line 115
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex_le_tableLength line 119
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_le_tableLength line 123
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_le_tableLength line 127
44. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frameContents line 135
45. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame0 line 149
46. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame1 line 151
47. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame2 line 153
48. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3 line 155
49. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame4 line 158
50. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame5 line 160
51. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame6 line 162
52. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame7 line 164
53. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8 line 166
54. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame9 line 169
55. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame10 line 171
56. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame11 line 173
57. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame12 line 175
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_id_eq line 178
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame1_eq line 186
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame2_eq line 192
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3_eq line 198
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame4_eq line 204
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame5_eq line 210
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame6_eq line 218
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame7_eq line 224
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8_eq line 231
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame9_eq line 238
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame10_eq line 245
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame11_eq line 253
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame12_eq line 261
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.final_frame_eq line 267
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame0_inputVertex line 272
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame0_table line 275
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame0_output line 278
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame1_inputVertex line 281
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame1_emitScratch line 284
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame2_queryReverse line 287
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame2_queryIndex line 290
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3_table line 293
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupRestore line 296
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupWork line 299
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupOutput line 302
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame3_queryIndex line 305
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame4_lookupOutput line 308
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame4_quotientFirst line 311
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame4_remainderFirst line 314
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame6_quotientFirst line 317
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame6_emitScratch line 320
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame7_queryReverse line 323
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame7_queryIndex line 326
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8_table line 329
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupRestore line 332
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupWork line 335
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupOutput line 338
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame8_queryIndex line 341
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame9_lookupOutput line 344
97. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame9_quotientSecond line 347
98. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame9_remainderSecond line 350
99. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame10_quotientSecond line 353
100. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame10_emitScratch line 356
101. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.frame10_output line 359
102. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.final_dirty_word_length_le line 362
103. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_le_tableLength line 370
104. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.concatenate line 382
105. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.rowSteps line 386
106. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.rowTraceAt line 404
107. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.rowSteps_le line 528
108. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.rowInTimeAt line 546
109. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderRow.rowInTime line 561
110. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_boundaryState line 579
111. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.prepareState_boundaryState line 583
112. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.clearRegister_boundaryState line 588
113. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_prepareState line 593
114. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_resetState line 596
115. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_clearRegister line 599
116. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_advancePositionState line 602
117. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller_resetPositionState line 605
118. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.nextPosition_val_of_lt line 608
119. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_update_count line 612
120. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes_increment_vertex line 622
121. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.initialTapes_initialize line 635
122. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.initializeStep line 649
123. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.initialize_boundaryStep line 658
124. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_succStep line 673
125. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_zeroStep line 685
126. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_succStep line 696
127. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexGuard_boundary_zeroStep line 709
128. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.prepareRowStep line 719
129. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.afterRow_moreStep line 727
130. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.afterRow_lastStep line 736
131. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.afterRow_last_boundaryStep line 746
132. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_consStep line 765
133. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.reverseOutput_nilStep line 777
134. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.doneStep line 789