OAI/Computability/MinUncut/Machines/PoweringMachineField.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.Tape line 13
2. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.State line 14
3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.Label line 16
4. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.labelFintype line 20
5. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.labelDecidableEq line 23
6. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.entry line 26
7. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.instruction line 30
8. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.finalTapes line 39
9. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.steps line 49
10. structure OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.Ready line 53
11. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.finalTapes_role line 61
12. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.ready_finalTapes line 76
13. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.finalTapes_other line 93
14. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.fieldTrace line 106
15. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineField.finalTapes_output line 128
16. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.Command line 160
17. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.LocalLabel line 161
18. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.Label line 162
19. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.entry line 164
20. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.instruction line 168
21. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.result line 175
22. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.finalTapes line 179
23. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.steps line 183
24. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.planTrace line 188
25. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.ready_finalTapes line 214
26. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.finalTapes_output line 227
27. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan line 248
28. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.boundedRowPlan_values line 255
29. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachinePlan.rowPlan_output line 260