OAI/Combinatorics/IndependentSets/Machines/MachineExpanderFamilyCycle.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.installed_returnFrame line 15
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.cleaned_multipliedFrame line 26
3. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.ResizeRun line 42
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.resizeInTime line 55
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.caller_initialState line 129
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.caller_normalizeState line 132
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_initialState line 135
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_update_level line 139
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initialTapes_initialize line 151
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.actualStep_of_boolStep line 168
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.bool_initializeStep line 181
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_succStep line 194
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_zeroStep line 207
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.bool_doneStep line 219
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initializeStep line 227
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_succStep line 239
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_zeroStep line 252
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.doneStep line 262
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.initialize_boundaryStep line 270
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_succStep line 286
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_zeroStep line 297