OAI/Combinatorics/IndependentSets/Machines/Remaining.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.remaining line 13
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.emittedPrefix line 15
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.remaining_step line 18
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.prefix_step line 26
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.remaining_zero line 33
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.remaining_end line 35
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.prefix_zero line 39
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.prefix_end line 41
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldFrame line 48
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderFrame line 57
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldVertexTrace line 65
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderVertexTrace line 83
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.tailCopyTrace line 114
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.tailFinishTrace line 131
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.pairSteps line 160
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.pairTrace line 166
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.cleanupSteps line 186
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.cleanupTrace line 188
19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.rawExpander line 217
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputPrefix line 220
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_step line 223
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.loopBase line 228
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.loopCost line 234
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.loopBodyTraces line 240
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.loopTrace line 276
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.tableSteps line 310
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.tableTrace line 315
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.flatMap_length_le line 343
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.flatten_length_le line 355
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldSize line 359
31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderSize line 360
32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.blockSize line 361
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.oldOutput_length_le line 363
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_length_le line 370
35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputBlock_length_le line 383
36. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputCapacity line 391
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_length_le line 393
38. def OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.pairBudget line 410
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineOverlayTable.pairSteps_le line 417