OAI/Computability/MinUncut/Machines/MachineRegularOwnerProgram.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.Tape line 15
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.Alphabet line 16
3. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.State line 17
4. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.Data line 18
5. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.CoreState line 19
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.MetaState line 20
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.FamilyState line 21
8. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable line 22
9. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 24) line 24
10. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 25) line 25
11. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.core line 27
12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.paddingTape line 28
13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.levelTape line 29
14. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.dummyFuel line 30
15. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.scratch line 31
16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.readyState line 33
17. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTape line 35
18. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView line 38
19. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyTape line 42
20. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyView line 45
21. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView line 49
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView_left line 53
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView_right line 56
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyView_left line 62
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyView_right line 65
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView_left line 71
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView_right line 73
28. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataStates line 79
29. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyStates line 85
30. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexStates line 91
31. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.Label line 97
32. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.entry line 109
33. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.program line 111
34. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working line 144
35. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.frame line 148
36. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cfg line 150
37. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.initialData line 153
38. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataData line 166
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.seededData line 169
40. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits line 172
41. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.finalData line 175
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.joinTrace line 186
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.oneStep line 190
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataPlacement line 194
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTrace line 204
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_local line 221
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_fuel line 235
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_global line 242
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working_update_output line 256
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.copyCountTrace line 270
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.copyFuelTrace line 286
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.guardZeroStep line 303
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.guardPositiveStep line 309
54. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.dummyBits line 318
55. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexData line 322
56. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopData line 329
57. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopFrame line 333
58. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.preSteps line 337
59. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopSteps line 341
60. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupCost line 348
61. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTime line 354
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyPlacement line 360
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyResultPlacement line 369
64. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyExecution line 380
65. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familySteps line 386
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.familyTrace line 390
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.coreFrame_eq line 410
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexPlacement line 428
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.vertexTrace line 443
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working_fuel line 467
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.working_scratch line 470
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopPositiveStep line 473
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopZeroStep line 484
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.bumpStep line 489
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopPrefixTrace line 499
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.preparationTrace line 527
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupFrame line 536
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits_zero line 577
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroFrame line 584
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopFrame line 594
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupZeroTrace line 605
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.cleanupLoopTrace line 619
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.loopTrace line 633
84. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerInTime line 648
85. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps line 680
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.ownerTrace line 683
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOwnerBody.totalSteps_le line 689
88. def OAI.MinUncutGames.Foundations.Complexity.naturalWordsEncoding line 697
89. def OAI.MinUncutGames.Foundations.Complexity.formulaEncoding line 702
90. def OAI.MinUncutGames.Foundations.Complexity.gameEncoding line 707
91. def OAI.MinUncutGames.Foundations.Complexity.prefixBitMachine line 712
92. def OAI.MinUncutGames.Foundations.Complexity.prefixBitPolyTime line 723
93. def OAI.MinUncutGames.Foundations.Complexity.enlargePolynomialBound line 742
94. def OAI.MinUncutGames.Foundations.Complexity.composeMachinePhases line 755
95. structure OAI.MinUncutGames.Foundations.Complexity.PolynomialGapReduction line 767