OAI/Combinatorics/IndependentSets/Machines/MachinePreservingLookupClean.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet line 14
2. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.Label line 16
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.statement line 21
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.program line 27
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.steps line 31
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.remaining_length_le line 35
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le line 42
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.timePolynomial line 50
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le_timePolynomial line 52
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt line 58
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt line 114
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.initialTapes_eq line 135
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt_fromTapes line 144
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.machine line 165
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePreservingLookupClean.machineInTime line 176