OAI/Computability/DirectedFeedback/Machines/MachineRegularTable.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.Extra line 58
2. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 62) line 62
3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.Tape line 64
4. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.Alphabet line 65
5. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.State line 66
6. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.tableTape line 68
7. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.nTape line 69
8. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.queryTape line 70
9. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.fuelTape line 71
10. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.sumTape line 72
11. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.mTape line 73
12. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.indexTape line 74
13. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.workTape line 75
14. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.scratchTape line 76
15. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.verticesTape line 77
16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.dartsTape line 78
17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.emitTape line 79
18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.outputTape line 80
19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.memory line 82
20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame line 94
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_table line 97
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_n line 99
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_query line 101
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_fuel line 103
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_sum line 105
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_m line 107
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_index line 109
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_work line 111
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_scratch line 113
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_vertices line 115
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_darts line 117
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_emit line 119
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.frame_output line 121
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_table line 124
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_n line 137
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_query line 150
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_fuel line 163
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_sum line 176
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_m line 189
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_index line 202
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_work line 215
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_scratch line 228
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_vertices line 241
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_darts line 254
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_emit line 267
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_output line 280
47. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.Field line 293
48. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 297) line 297
49. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase line 299
50. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 303) line 303
51. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.Label line 305
52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.fieldTape line 315
53. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.fieldExit line 319
54. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots line 323
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots_injective line 326
56. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.copySource line 331
57. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.copyDestination line 336
58. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.copyExit line 340
59. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.prefixView line 345
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_left line 349
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_right line 351
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.prefixTapes line 355
63. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.program line 366
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.appendTrace_inline_MachineRegularTable line 396
65. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.paddingTotal line 400
66. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal line 403
67. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.dartTotal line 406
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal_eq line 408
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.initStep line 413
70. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.seedMStep line 422
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.clearIndexStep line 431
72. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.readTime line 440
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.readTrace line 444
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.prefixTrace line 491
75. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.computeTime line 511
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.computeTrace line 514
77. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.headerBits line 552
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_eq line 555
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_length line 559
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.cleanupZerosStep line 565
81. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.emitTime line 574
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.emitTrace line 578
83. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.totalTime line 641
84. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.trace line 644
85. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.arithmeticPolynomial line 657
86. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.timePolynomial line 664
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.totalTime_le line 667
88. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Header.inTime line 709
89. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Fuel.guard line 729
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_succ line 737
91. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_zero line 744
92. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Fuel.increment line 751
93. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Fuel.increment_step line 754
94. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.Body line 764
95. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.Tape line 765
96. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.Alphabet line 766
97. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.State line 767
98. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.Data line 768
99. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable line 769
100. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.sumDecidableEq_inline_MachineRegularTable line 771
101. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.tapeDecidableEq line 782
102. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.tapeBEq line 797
103. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.tapeLawfulBEq line 800
104. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.tapeFintype line 804
105. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.coreTape line 812
106. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldFuel line 813
107. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerFuel line 814
108. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.dummyFuel line 815
109. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.scratch line 816
110. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerTape line 818
111. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerView line 824
112. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerView_left line 835
113. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerView_right line 844
114. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.bodyView line 863
115. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_left line 867
116. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_right line 868
117. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerTape line 874
118. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerView line 878
119. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_left line 886
120. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_right line 892
121. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.headerStates line 901
122. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.readyState line 909
123. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase line 911
124. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.(instance at line 914) line 914
125. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.copySource line 916
126. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.copyTarget line 919