OAI/Computability/BinPacking/Computation/MachineCloudSelect.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.BaseTape line 10
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.BaseAlphabet line 11
3. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.BaseState line 12
4. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.BaseLabel line 14
5. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.skipLabel line 20
6. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.baseProgram line 25
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.baseProgram_skip line 45
8. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Phase line 50
9. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList line 54
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_getElem?_ctorIdx_eq line 56
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Phase.enumList_nodup line 60
12. instance OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.(instance at line 62) line 62
13. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Control line 65
14. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Control.enumList line 69
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_getElem?_ctorIdx_eq line 71
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Control.enumList_nodup line 75
17. instance OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.(instance at line 77) line 77
18. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Tape line 81
19. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Alphabet line 82
20. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.Label line 83
21. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.State line 84
22. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.go line 86
23. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.dispatcher line 89
24. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.extra line 102
25. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.program line 106
26. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.memory line 109
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.memory_inl line 114
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.memory_position line 116
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.update_memory_hit line 119
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.update_memory_rank line 125
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.update_memory_position line 131
32. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.cfg line 138
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.liftTrace line 143
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.compareTrace line 156
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.dispatch_miss line 179
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_succ line 186
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.dispatch_hit_zero line 195
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.advanceStep line 203
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.finishStep line 212
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.initializeStep line 218
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.skipTrace line 225
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.rowSkipTrace line 249
43. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.prefixTime line 293
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.prefixTrace line 297
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.cleanupTrace line 325
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.selectedTrace line 359
47. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.queryWord line 376
48. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.prepareSteps line 378
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.prepareTrace line 382
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.prefixSelectedTrace line 441
51. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.totalSteps line 463
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.fullTrace line 468
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.prefixTime_le line 492
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.totalSteps_le line 504
55. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.remainder line 522
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.tableRows_getElem line 526
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.tableWord_split line 536
58. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps line 549
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.cloudSelectTrace line 555
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.cloudSelectSteps_le line 579
61. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.timePolynomial line 589
62. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.cloudSelectInTime line 592
63. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.machine line 608
64. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudSelect.machineInTime line 619