OAI/Combinatorics/IndependentSets/Machines/Tape2.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.Tape line 16
2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.Ambient line 17
3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.State line 18
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.graphArchive line 20
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.graphStream line 21
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.scratch line 22
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.vertexCount line 23
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.dartCount line 24
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderArchive line 25
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderStream line 26
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.fuel line 27
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.vertex line 28
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.tail line 29
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldReverse line 30
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.relation line 31
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.dividedCopy line 32
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.quotient line 33
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.newReverse line 34
19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.rowBuffer line 35
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.output line 36
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldTapes line 38
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderTapes line 42
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldTapes_injective line 46
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderTapes_injective line 52
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.clean line 58
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderState line 61
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderState_clean line 70
28. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.MainLabel line 75
29. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.Label line 87
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.next line 89
31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.mainInstruction line 91
32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.program line 131
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.program_main line 137
34. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.extraTapes line 140
35. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.splitView line 143
36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.combine line 147
37. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.initialTapes line 151
38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.splitTapes line 154
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.placedTapes line 157
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.splitTrace line 162
41. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory line 182
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_graphArchive line 186
43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_graphStream line 188
44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_scratch line 190
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_vertexCount line 192
46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_dartCount line 194
47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_expanderArchive line 196
48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_expanderStream line 198
49. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_fuel line 200
50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_vertex line 202
51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_tail line 204
52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_oldReverse line 206
53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_relation line 208
54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_dividedCopy line 210
55. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_quotient line 212
56. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_newReverse line 214
57. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_rowBuffer line 216
58. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.memory_output line 218
59. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_output line 221
60. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_expanderStream line 224
61. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_graphStream line 228
62. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_fuel line 232
63. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_vertex line 235
64. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_tail line 238
65. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_vertexCount line 241
66. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.update_dartCount line 244
67. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.joinTrace line 248
68. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.initialTapes_memory line 252
69. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.splitTapes_memory line 259
70. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.preparationSteps line 267
71. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.preparationTrace line 269
72. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatMap line 337
73. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten line 343
74. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_flatMap line 349
75. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldRows line 358
76. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderValues line 359
77. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldBlock line 362
78. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderBlock line 364
79. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldOutput line 367
80. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderOutput line 369
81. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputBlock line 371
82. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldOutput_eq line 374
83. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_eq line 388
84. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputBlock_eq line 392
85. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.graphRows_blocks line 398
86. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderRows_blocks line 407
87. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.tableBits_blocks line 412