OAI/Computability/MinUncut/Machines/MachineRegularOriginalBody.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.Tape line 14
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.Alphabet line 15
3. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.CoreState line 16
4. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.MetaState line 17
5. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.FamilyState line 18
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.State line 19
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.Data line 20
8. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable line 21
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive line 23
10. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.readyState line 26
11. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTape line 30
12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView line 34
13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyTape line 39
14. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyView line 43
15. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView line 48
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_left line 52
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_right line 55
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_left line 63
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_right line 66
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_left line 74
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_right line 76
22. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataStates line 82
23. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyStates line 88
24. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexStates line 89
25. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.Label line 92
26. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.entry line 99
27. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearTape line 101
28. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearEntry line 105
29. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearSource line 108
30. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSource line 111
31. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.program line 115
32. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.frame line 126
33. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame line 131
34. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.cfg line 134
35. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.initialData line 137
36. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData line 150
37. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyData line 153
38. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits line 158
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData line 161
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.joinTrace line 165
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataPlacement line 169
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTrace line 177
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyPlacement line 193
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyResultPlacement line 201
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyExecution line 214
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familySteps line 219
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.familyTrace line 223
48. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearMemory line 240
49. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearSteps line 245
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.identityPlacement line 250
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.drainTrace line 253
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearPrefixTrace line 269
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearTrace line 284
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.clearFrame line 290
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame_eq line 308
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData_eq line 328
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexPlacement line 332
58. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps line 343
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.vertexTrace line 347
60. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps line 366
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.originalTrace line 371
62. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalBody.originalExecution line 387
63. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape line 405
64. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.State line 406
65. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet line 407
66. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.sumDecidableEq line 409
67. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeDecidableEq line 420
68. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeBEq line 432
69. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeLawfulBEq line 435
70. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeFintype line 439
71. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.core line 446
72. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.localRank line 447
73. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.count line 448
74. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape line 449
75. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.rotor line 450
76. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding line 451
77. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.level line 452
78. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel line 453
79. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch line 454
80. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes line 456
81. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label line 458
82. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.entry line 464
83. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry line 466
84. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction line 469
85. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.afterAddition line 478
86. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes line 481
87. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps line 484
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_apply line 487
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_prefix line 494
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_empty line 499
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_other line 503
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_scratch line 508
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.drainSteps_eq line 514
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.additionTraceAt line 520
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.traceAt line 545
96. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerCleanup.executionAt line 565