OAI/Combinatorics/IndependentSets/Machines/MachineTransducerCopy.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.Alphabet line 14
2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.State line 15
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.scanLoop line 17
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.emitter line 26
5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.tapes line 32
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.update_source line 36
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.update_scratch line 51
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.update_output line 63
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.scanStep_empty line 69
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.scanStep_cons line 87
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.emitterStep line 105
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.twoSteps_cons line 126
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.scanTrace line 152
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.restoreTapes line 186
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyTrace line 205
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyInTime line 251
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.scanLoop_pushBound line 277
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineTransducerCopy.emitter_pushBound line 283