OAI/Computability/MinUncut/Estimates/Basic2.lean

GitHub source file

151 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Extra line 16
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList line 20
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_getElem?_ctorIdx_eq line 23
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_nodup line 27
5. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 29) line 29
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Tape line 33
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Alphabet line 34
8. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.State line 35
9. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.tableTape line 37
10. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.nTape line 38
11. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.queryTape line 39
12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.fuelTape line 40
13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.sumTape line 41
14. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.mTape line 42
15. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.indexTape line 43
16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.workTape line 44
17. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.scratchTape line 45
18. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.verticesTape line 46
19. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.dartsTape line 47
20. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.emitTape line 48
21. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.outputTape line 49
22. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.memory line 51
23. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame line 63
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_table line 66
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_n line 68
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_query line 70
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_fuel line 72
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_sum line 74
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_m line 76
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_index line 78
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_work line 80
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_scratch line 82
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_vertices line 84
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_darts line 86
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_emit line 88
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.frame_output line 90
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_table line 93
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_n line 106
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_query line 119
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_fuel line 132
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_sum line 145
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_m line 158
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_index line 171
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_work line 184
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_scratch line 197
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_vertices line 210
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_darts line 223
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_emit line 236
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_output line 249
50. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Field line 262
51. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList line 266
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_getElem?_ctorIdx_eq line 268
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_nodup line 272
54. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 274) line 274
55. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase line 278
56. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList line 282
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_getElem?_ctorIdx_eq line 284
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_nodup line 288
59. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 290) line 290
60. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.Label line 294
61. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.fieldTape line 304
62. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.fieldExit line 308
63. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots line 312
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots_injective line 315
65. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.copySource line 320
66. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.copyDestination line 325
67. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.copyExit line 329
68. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.prefixView line 334
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_left line 338
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_right line 340
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.prefixTapes line 344
72. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.program line 355
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.appendTrace line 385
74. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.paddingTotal line 389
75. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal line 392
76. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.dartTotal line 395
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal_eq line 397
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.initStep line 402
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.seedMStep line 411
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.clearIndexStep line 420
81. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.readTime line 429
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.readTrace line 433
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.prefixTrace line 480
84. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.computeTime line 500
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.computeTrace line 503
86. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits line 541
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_eq line 544
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_length line 548
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.cleanupZerosStep line 554
90. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.emitTime line 563
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.emitTrace line 567
92. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.totalTime line 630
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.trace line 633
94. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.arithmeticPolynomial line 646
95. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.timePolynomial line 653
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.totalTime_le line 656
97. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Header.inTime line 698
98. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard line 718
99. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_succ line 726
100. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_zero line 733
101. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Fuel.increment line 740
102. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Fuel.increment_step line 743
103. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.Body line 753
104. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.Tape line 754
105. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.Alphabet line 755
106. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.State line 756
107. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.Data line 757
108. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable line 758
109. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.sumDecidableEq line 760
110. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.tapeDecidableEq line 771
111. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.tapeBEq line 786
112. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.tapeLawfulBEq line 789
113. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.tapeFintype line 793
114. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.coreTape line 801
115. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.oldFuel line 802
116. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerFuel line 803
117. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.dummyFuel line 804
118. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.scratch line 805
119. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerTape line 807
120. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerView line 813
121. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerView_left line 824
122. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerView_right line 833
123. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.bodyView line 852
124. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_left line 856
125. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_right line 857
126. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerTape line 863
127. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerView line 867
128. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_left line 875
129. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_right line 881
130. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerStates line 890
131. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.readyState line 898
132. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase line 900
133. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList line 904
134. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_getElem?_ctorIdx_eq line 906
135. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_nodup line 910
136. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.(instance at line 912) line 912
137. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.copySource line 916
138. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.copyTarget line 919
139. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.Label line 923
140. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.copyExit line 938
141. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.clearTape line 942
142. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.clearEntry line 946
143. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.program line 949
144. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.machine line 969
145. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame line 980
146. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.cfg line 986
147. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.frame_core line 991
148. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.bodyPlacement line 995
149. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerAux line 1004
150. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerAux_empty line 1010
151. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Top.headerPlacement line 1014