OAI/Combinatorics/IndependentSets/Machines/MachinePaddedOverlayRuntime.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.rawProgram line 12
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.sourceMachine_eq line 20
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanupTapes line 24
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.cleanup_complete line 27
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.initial_configuration line 31
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.terminalRun line 40
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.computableInPolyTime line 52
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePaddedOverlayRuntime.finite_alphabet line 61
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyCodec.rowsBits_ofFn line 72
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyCodec.encodeWords_flatMap line 89
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyCodec.rowBits_stay line 95
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyCodec.rowsBits_stay line 102