OAI/Computability/BinPacking/Computation/MachinePaddedOverlayRuntime.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.BaseTable line 12
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.baseDegree line 13
3. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree line 14
4. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.Tape line 15
5. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.Alphabet line 16
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.Label line 17
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.State line 18
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayDegree_positive line 20
9. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddingTape line 23
10. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddingView line 25
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_left line 29
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddingView_right line 31
13. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyTape line 37
14. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyView line 40
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyView_left line 45
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyView_right line 50
17. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayTape line 58
18. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayView line 63
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_left line 70
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayView_right line 77
21. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddingLabel line 97
22. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyLabel line 98
23. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayLabel line 99
24. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.main line 100
25. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyEntry line 101
26. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayEntry line 102
27. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyStates line 104
28. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayStates line 112
29. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familySource line 120
30. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlaySource line 125
31. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.program line 130
32. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.clean line 137
33. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.memory line 141
34. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.padded line 148
35. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.rotor line 151
36. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.initialTapes line 155
37. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddedTapes line 158
38. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyTapes line 162
39. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.finalTapes line 166
40. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.placeExecution line 171
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.padding_initial_memory line 187
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.padding_final_memory line 199
43. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.paddingInTime line 211
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.family_initial_memory line 224
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.family_final_memory line 247
46. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyInTime line 276
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.rotationWords_resize line 334
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.rotor_familyAt line 340
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlay_memory line 345
50. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.overlayInTime line 366
51. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.sizePolynomial line 402
52. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.archivePolynomial line 405
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.archive_length_le line 411
54. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.familyPolynomial line 436
55. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.timePolynomial line 439
56. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.execution line 443
57. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.machine line 469
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.alphabet_finite line 480
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.initial_configuration line 486
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.final_output line 502
61. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlay.original_preserved line 508
62. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram line 519
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.sourceMachine_eq line 527
64. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanupTapes line 531
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanup_complete line 534
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.initial_configuration line 538
67. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.terminalRun line 547
68. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime line 559
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedOverlayRuntime.finite_alphabet line 568