OAI/Computability/MinUncut/Machines/MachinePaddedOverlay.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable line 13
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.baseDegree line 14
3. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree line 15
4. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.Tape line 16
5. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.Alphabet line 17
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.Label line 18
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.State line 19
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree_positive line 21
9. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddingTape line 24
10. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddingView line 26
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_left line 30
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_right line 32
13. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyTape line 38
14. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyView line 41
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyView_left line 46
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyView_right line 51
17. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayTape line 59
18. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayView line 64
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_left line 71
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_right line 78
21. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddingLabel line 98
22. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyLabel line 99
23. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayLabel line 100
24. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.main line 101
25. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyEntry line 102
26. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayEntry line 103
27. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyStates line 105
28. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayStates line 113
29. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familySource line 121
30. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlaySource line 126
31. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.program line 131
32. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.clean line 138
33. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.memory line 142
34. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.padded line 149
35. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.rotor line 152
36. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.initialTapes line 156
37. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddedTapes line 159
38. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyTapes line 163
39. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.finalTapes line 167
40. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.placeExecution line 172
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.padding_initial_memory line 188
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.padding_final_memory line 200
43. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.paddingInTime line 212
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.family_initial_memory line 225
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.family_final_memory line 248
46. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyInTime line 277
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.rotationWords_resize line 335
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.rotor_familyAt line 341
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlay_memory line 348
50. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.overlayInTime line 369
51. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.sizePolynomial line 405
52. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.archivePolynomial line 408
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.archive_length_le line 414
54. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.familyPolynomial line 439
55. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.timePolynomial line 442
56. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.execution line 446
57. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.machine line 472
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.alphabet_finite line 483
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.initial_configuration line 489
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.final_output line 506
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlay.original_preserved line 512
62. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram line 526
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.sourceMachine_eq line 534
64. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanupTapes line 538
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanup_complete line 541
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.initial_configuration line 545
67. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.terminalRun line 554
68. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime line 566
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedOverlayRuntime.finite_alphabet line 575
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyCodec.rowsBits_ofFn line 589
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyCodec.encodeWords_flatMap line 606
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyCodec.rowBits_stay line 612
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLazyCodec.rowsBits_stay line 619