OAI/Computability/MinUncut/Machines/SelectorMachine.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps_le line 13
2. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectorMachine line 34
3. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectionInTime line 45
4. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes line 65
5. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes line 67
6. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectTape line 69
7. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView line 87
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_left line 96
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectView_right line 104
10. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTape line 109
11. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorStateEquiv line 111
12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectStateEquiv line 120
13. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreAfterCleanup line 127
14. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreInstruction line 131
15. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreInitialState line 145
16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreMachine line 149
17. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory line 160
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreMemory_update_output line 166
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTapes_injective line 174
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTapes_injective line 178
21. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned line 182
22. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps line 187
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupTrace line 192
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleaned_memory line 269
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreCleanupSteps_memory line 277
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorFinalFrame line 289
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreRotorTrace line 305
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectFrame line 351
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSelectionTrace line 360
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreFinishTrace line 395
31. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreInputTapes line 427
32. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps line 437
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreTrace line 451
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectedIndex_le line 498
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.encodedDrop_length_le line 509
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorSize_le_encodedLength line 516
37. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreTimeBound line 524
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreSteps_le line 528
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreMachineInTime line 592
40. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.Tape line 620
41. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.Alphabet line 621
42. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.State line 622
43. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.Label line 624
44. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.instruction line 629
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTapes line 639
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps line 643
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.join_trace line 647
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTraceAt line 651
49. structure OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.Input line 685
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanup_frame line 690
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.suffix_length_le line 704
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_eq line 714
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_le line 758
54. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.steps line 772
55. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.timeBound line 776
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.steps_le line 779
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.traceAt line 787
58. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.machine line 806
59. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalClean.machineInTime line 817