OAI/Computability/MinUncut/Machines/MachineExpanderTableProgram.lean

GitHub source file

171 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape line 11
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList line 15
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_getElem?_ctorIdx_eq line 17
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.ExtraTape.enumList_nodup line 21
5. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.(instance at line 23) line 23
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.Tape line 27
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.Alphabet line 29
8. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.alphabetFintype line 33
9. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel line 36
10. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList line 40
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_getElem?_ctorIdx_eq line 43
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.OuterLabel.enumList_nodup line 47
13. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.(instance at line 49) line 49
14. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.Label line 53
15. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.Position line 54
16. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.State line 55
17. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.RowStatePrefix line 56
18. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.guardStates line 59
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.guardStates_apply line 66
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.guardStates_symm_apply line 70
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowFactor_pos line 73
22. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.zeroPosition line 77
23. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.nextPosition line 80
24. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.positionPair line 83
25. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.caller line 86
26. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.boundaryState line 88
27. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.initialState line 93
28. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.prepareState line 97
29. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.resetState line 101
30. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.clearRegister line 105
31. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.advancePositionState line 108
32. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.resetPositionState line 111
33. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.vertexGuardCore line 114
34. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.outerStatement line 124
35. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowReturn line 144
36. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.program line 146
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.program_row line 151
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.program_outer line 157
39. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowExecution line 161
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowExecution_steps line 173
41. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.rowTapes line 181
42. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.extraTapes line 187
43. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.boundaryTapes line 191
44. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.initialTapes line 195
45. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderTable.finalTapes line 201
46. def OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.tapes line 213
47. def OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.statement line 215
48. def OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration line 217
49. def OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.program line 219
50. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.castStatement line 222
51. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.castConfiguration line 223
52. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.castProgram line 224
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.tapes_rfl line 226
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.statement_rfl line 227
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_rfl line 228
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.program_rfl line 229
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.program_apply line 231
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.statement_roundtrip line 234
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.statement_symm_roundtrip line 237
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_roundtrip line 240
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_symm_roundtrip line 243
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.program_roundtrip line 246
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.program_symm_roundtrip line 249
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.tapes_roundtrip line 252
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.tapes_symm_roundtrip line 255
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_label line 258
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_state line 261
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_tapes line 264
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.configuration_mk line 267
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.map_configuration_rfl line 271
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.stepAux_simulation line 276
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.step_simulation line 281
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.trace_transport line 287
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.successfulTrace line 295
75. def OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime line 303
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.executionInTime_steps line 315
77. def OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime line 320
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAlphabetTransport.successfulExecutionInTime_steps line 326
79. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape line 338
80. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList line 342
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_getElem?_ctorIdx_eq line 345
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.ExtraTape.enumList_nodup line 349
83. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 351) line 351
84. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.Tape line 355
85. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.Alphabet line 356
86. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.BoolAlphabet line 358
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.alphabet_eq line 360
88. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.alphabetFintype line 366
89. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase line 370
90. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList line 374
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_getElem?_ctorIdx_eq line 376
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffinePhase.enumList_nodup line 380
93. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 382) line 382
94. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel line 386
95. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList line 390
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_getElem?_ctorIdx_eq line 392
97. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.AffineLabel.enumList_nodup line 396
98. instance OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.(instance at line 398) line 398
99. inductive OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.OuterLabel line 402
100. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.Label line 410
101. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.State line 411
102. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.RegisterAmbient line 412
103. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.registerStates line 415
104. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.registerStates_apply line 422
105. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.registerStates_symm_apply line 426
106. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.caller line 429
107. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initialState line 432
108. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.normalizeState line 436
109. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding line 440
110. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initialEncoding_eq_family line 442
111. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.tableTape line 445
112. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.inputVertexTape line 446
113. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.vertexCountTape line 447
114. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.resultTape line 448
115. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineSource line 450
116. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineDestination line 454
117. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineCoefficient line 458
118. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineExit line 462
119. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.affineStatement line 466
120. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.drainStatement line 484
121. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boolOuterStatement line 492
122. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.outerStatement line 521
123. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.tableReturn line 525
124. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.program line 527
125. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.program_table line 532
126. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.program_outer line 539
127. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boolView line 543
128. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boolView_outer line 547
129. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.tableExecution line 556
130. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.tableExecution_steps line 568
131. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.tableFrame line 577
132. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.extraFrame line 583
133. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes line 588
134. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes line 592
135. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.familyTapes line 599
136. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boolWord line 606
137. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord line 611
138. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes line 616
139. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes line 619
140. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBoolWord_boolWord line 622
141. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boolWord_toBoolWord line 628
142. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBool_fromBool line 634
143. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.fromBool_toBool line 639
144. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.transport_tapes_apply line 644
145. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_eq_transport line 651
146. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_eq_transport line 659
147. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.fromBoolTapes_update line 667
148. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.toBoolTapes_update line 676
149. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.configuration_fromBool line 686
150. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.configuration_toBool line 692
151. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.controlStatementInverse line 701
152. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.controlTrace line 708
153. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.controlDrainTrace line 732
154. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.controlTransferTrace line 751
155. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister line 776
156. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.registerStates_reset line 779
157. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_idempotent line 783
158. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.caller_clearRegister line 786
159. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_position line 789
160. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_register line 792
161. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boolTraceActual line 797
162. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.drainBoolTrace line 808
163. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.transferBoolTrace line 825
164. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.installedTapes line 848
165. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cleanedCounterTapes line 855
166. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.installTableBoolTrace line 858
167. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersBoolTrace line 917
168. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.installTableTrace line 935
169. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersTrace line 948
170. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.installTableInTime line 959
171. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cleanupCountersInTime line 974