OAI/Computability/DirectedFeedback/Machines/MachinePaddedOverlay.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable line 58
2. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.baseDegree line 59
3. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree line 60
4. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.Tape line 61
5. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.Alphabet line 62
6. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.Label line 63
7. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.State line 64
8. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree_positive line 66
9. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddingTape line 69
10. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddingView line 71
11. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_left line 75
12. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_right line 77
13. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyTape line 83
14. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyView line 86
15. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyView_left line 91
16. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyView_right line 96
17. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayTape line 104
18. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayView line 109
19. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_left line 116
20. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_right line 123
21. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddingLabel line 141
22. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyLabel line 142
23. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayLabel line 143
24. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.main line 144
25. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyEntry line 145
26. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayEntry line 146
27. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyStates line 148
28. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayStates line 156
29. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familySource line 164
30. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlaySource line 169
31. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.program line 174
32. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.clean line 181
33. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.memory line 185
34. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.padded line 192
35. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.rotor line 195
36. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.initialTapes line 199
37. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddedTapes line 202
38. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyTapes line 206
39. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.finalTapes line 210
40. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.placeExecution_inline_MachinePaddedOverlay line 215
41. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.padding_initial_memory line 231
42. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.padding_final_memory line 243
43. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.paddingInTime line 255
44. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.family_initial_memory line 268
45. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.family_final_memory line 291
46. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyInTime line 320
47. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.rotationWords_resize line 378
48. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.rotor_familyAt line 384
49. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlay_memory line 391
50. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.overlayInTime line 413
51. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.sizePolynomial line 449
52. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.archivePolynomial line 452
53. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.archive_length_le line 458
54. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.familyPolynomial line 483
55. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.timePolynomial line 486
56. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.execution line 490
57. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.machine line 516
58. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.alphabet_finite line 527
59. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.initial_configuration line 533
60. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.final_output line 550
61. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlay.original_preserved line 556
62. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram line 570
63. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.sourceMachine_eq line 578
64. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanupTapes line 582
65. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanup_complete line 585
66. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.initial_configuration line 589
67. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.terminalRun line 598
68. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime line 610
69. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedOverlayRuntime.finite_alphabet line 619
70. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyCodec.rowsBits_ofFn line 634
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyCodec.encodeWords_flatMap_inline_MachineLazyCodec line 651
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyCodec.rowBits_stay line 657
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyCodec.rowsBits_stay line 664