OAI/Combinatorics/IndependentSets/Machines/MachineCopy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.Alphabet line 14
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkLoop line 16
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkTapes line 24
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkTapes_source line 29
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkTapes_left line 35
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkTapes_right line 40
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkTapes_self line 45
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.update_fork_source line 49
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.update_fork_left line 63
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.update_fork_right line 74
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkStep_empty line 80
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkStep_cons line 96
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkTrace line 114
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.forkInTime line 141
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.drainedTapes line 161
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.restoredTapes line 164
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.copyTrace line 182
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineCopy.copyInTime line 223