OAI/Combinatorics/IndependentSets/Machines/MachineLazyTableRuntime.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.rawProgram line 11
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.sourceMachine_eq line 19
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.cleanupTapes line 23
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.cleanup_complete line 27
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.terminalRun line 31
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime line 41
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLazyTableRuntime.finite_alphabet line 48
8. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingFinishRuntime.finish line 60
9. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingFinishRuntime.output_eq_finish line 65
10. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingFinishRuntime.finish_degree_positive line 69
11. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingFinishRuntime.computableInPolyTime line 72
12. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingFinishRuntime.finite_alphabet line 83
13. def OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRuntime.tablePolynomialTime line 98
14. theorem OAI.IndependentSetsGames.Foundations.PCP.PreprocessingRuntime.finiteAlphabet line 111