OAI/Combinatorics/IndependentSets/Machines/MachineStateFrame.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameStatement line 12
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameConfiguration line 24
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameProgram line 27
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_state line 30
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_metadata line 33
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_tapes line 36
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameStatement_pushBound line 39
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.statement line 43
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.configuration line 47
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.configuration_state line 51
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.configuration_metadata line 55
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.configuration_tapes line 59
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.statement_pushBound line 63
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frame_stepAux line 73
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frame_step line 94
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frame_advance line 106
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frame_iterate line 115
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameExecution line 127
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.frameExecution_steps line 141
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.stepAux_simulation line 146
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.step_simulation line 153
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.trace line 166
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.execution line 177
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineStateFrame.execution_steps line 187