OAI/Computability/VertexCover/Encoding/MachineEmbedding.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.Alphabet line 45
2. def OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.tapes line 49
3. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.tapes_inl line 54
4. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.tapes_inr line 57
5. def OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.label line 60
6. def OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.configuration line 64
7. def OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.statement line 71
8. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.tapes_update line 88
9. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 101
10. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 127
11. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 135
12. def OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.program line 143
13. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.step_running line 149
14. theorem OAI.UniqueGames.Foundations.Complexity.MachineEmbedding.step_simulation line 162