OAI/Combinatorics/IndependentSets/Machines/MachineUnaryAffine.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.Alphabet line 15
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.finish line 17
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.scan line 20
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.seed line 30
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.tapes line 34
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_source line 38
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_scratch line 44
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_destination line 49
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.update_source line 54
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.update_scratch line 68
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.update_destination line 79
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.prepend_replicate_word line 85
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_succ line 90
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_zero line 110
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.scanTrace line 127
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.restoreTapes line 157
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.affineTrace line 176
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.affineInTime line 212
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.seededAffineTrace line 232
20. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.Label line 266
21. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.(instance at line 270) line 270
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.program line 274
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineUnaryAffineAt.machine line 280