OAI/Combinatorics/IndependentSets/Machines/MachineRegularTableRuntime.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.rawProgram line 13
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.sourceMachine_eq line 21
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.cleanupTapes line 25
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.cleanup_complete line 28
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.terminalRun line 32
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime line 52
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTableRuntime.finite_alphabet line 60
8. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.Tape line 71
9. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.State line 72
10. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.Label line 74
11. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.(instance at line 78) line 78
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.tapes line 82
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.initialTapes line 86
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.resultTapes line 88
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.resultTapes_original line 91
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.resultTapes_work line 95
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.resultTapes_scratch line 98
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.resultTapes_vertices line 101
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.resultTapes_darts line 104
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.program line 107
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.exactSteps line 115
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.splitTrace line 118
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.timePolynomial line 188
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.timePolynomial_eval line 190
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.exactSteps_le line 193
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.splitInTime line 200
27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.machine line 210
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.initial_configuration line 221
29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.rowsBits line 229
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.tableBits_header_rows line 232
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.tableTrace line 236
32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTableSplit.initializedTableInTime line 244