OAI/Combinatorics/IndependentSets/Machines/MachineFixedBlockMap.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.Buffer line 10
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer line 12
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.readSlots line 18
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.fill line 27
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.fill_apply line 30
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.fill_all line 41
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readSlots line 48
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readAll line 64
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_readSlots line 78
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.writeSlots line 86
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_writeSlots line 91
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_writeSlots line 106
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.blockStmt line 122
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.finishAt line 129
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt line 134
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockStmt line 138
17. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockMapAt line 145
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockStmt line 153
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockMapAt line 167
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.step_blockMapAt line 178
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.machine line 195
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFixedBlockMap.machine_statementPushBound line 206