OAI/Computability/MinUncut/Machines/MachineCloudSelect.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.BaseTape line 12
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.BaseAlphabet line 13
3. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.BaseState line 14
4. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.BaseLabel line 16
5. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.skipLabel line 22
6. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.baseProgram line 27
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.baseProgram_skip line 47
8. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Phase line 52
9. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList line 56
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_getElem?_ctorIdx_eq line 58
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_nodup line 62
12. instance OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.(instance at line 64) line 64
13. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Control line 67
14. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Control.enumList line 71
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_getElem?_ctorIdx_eq line 73
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_nodup line 77
17. instance OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.(instance at line 79) line 79
18. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Tape line 83
19. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Alphabet line 84
20. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.Label line 85
21. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.State line 86
22. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.go line 88
23. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.dispatcher line 91
24. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.extra line 104
25. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.program line 108
26. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.memory line 111
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.memory_inl line 116
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.memory_position line 118
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.update_memory_hit line 121
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.update_memory_rank line 127
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.update_memory_position line 133
32. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.cfg line 140
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.liftTrace line 145
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.compareTrace line 158
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.dispatch_miss line 181
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_succ line 188
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_zero line 197
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.advanceStep line 205
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.finishStep line 214
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.initializeStep line 220
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.skipTrace line 227
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.rowSkipTrace line 251
43. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.prefixTime line 295
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.prefixTrace line 299
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.cleanupTrace line 327
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.selectedTrace line 361
47. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.queryWord line 378
48. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.prepareSteps line 380
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.prepareTrace line 384
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.prefixSelectedTrace line 443
51. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.totalSteps line 465
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.fullTrace line 470
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.prefixTime_le line 494
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.totalSteps_le line 506
55. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.remainder line 524
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.tableRows_getElem line 528
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.tableWord_split line 538
58. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps line 551
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectTrace line 557
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps_le line 581
61. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.timePolynomial line 591
62. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.cloudSelectInTime line 594
63. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.machine line 610
64. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudSelect.machineInTime line 621