OAI/Computability/MinUncut/Machines/MachineSubroutine.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.label line 12
2. def OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.configuration line 16
3. def OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.statement line 19
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.stepAux_simulation line 33
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.step_simulation line 54
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.trace line 70
7. def OAI.MinUncutGames.Foundations.Complexity.MachineSubroutine.execution line 80
8. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameStatement line 98
9. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration line 110
10. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameProgram line 113
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_state line 116
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_metadata line 119
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_tapes line 122
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameStatement_pushBound line 125
15. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.statement line 129
16. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.configuration line 133
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.configuration_state line 137
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.configuration_metadata line 141
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.configuration_tapes line 145
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.statement_pushBound line 149
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frame_stepAux line 159
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frame_step line 180
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frame_advance line 192
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frame_iterate line 201
25. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameExecution line 213
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.frameExecution_steps line 227
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.stepAux_simulation line 232
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.step_simulation line 239
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.trace line 252
30. def OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.execution line 263
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineStateFrame.execution_steps line 273