OAI/Combinatorics/IndependentSets/Machines/MachineLookupCore.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.Alphabet line 13
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.discard line 15
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.select line 22
4. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.Label line 29
5. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.(instance at line 33) line 33
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.program line 37
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.tapes line 46
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.tapes_index line 51
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.tapes_source line 57
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.tapes_destination line 63
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.tapes_other line 68
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.update_index line 74
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.update_source line 88
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.update_destination line 99
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.fieldTapes_eq line 105
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineLookup.machine line 112