OAI/Combinatorics/IndependentSets/Machines/PoweringMachineWord.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.Alphabet line 15
2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.Tape line 16
3. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.first line 18
4. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.shift line 20
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.shift_injective line 22
6. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.rotorRole line 26
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.rotorRole_injective line 31
8. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.Label line 35
9. instance OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.labelFintype line 39
10. instance OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.labelDecidableEq line 46
11. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.entry line 53
12. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.copyInstruction line 57
13. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.instruction line 64
14. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.steps line 77
15. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.finalTapes line 83
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.finalTapes_other line 92
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.wordTrace line 111
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.steps_le line 186
19. def OAI.IndependentSetsGames.Foundations.Complexity.PoweringMachineWord.machine line 200