OAI/Combinatorics/IndependentSets/Machines/MachineEmbedding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.Alphabet line 11
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.tapes line 15
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.tapes_inl line 20
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.tapes_inr line 23
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.label line 26
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.configuration line 30
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.statement line 37
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.tapes_update line 54
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 67
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 93
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 101
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.program line 109
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.step_running line 115
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineEmbedding.step_simulation line 128