OAI/Combinatorics/IndependentSets/Machines/MachinePortReindex.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.Alphabet line 15
2. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.State line 16
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.clean line 18
4. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.Label line 21
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.exitAt line 27
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.emit line 33
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.instruction line 38
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.steps line 59
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.steps_le line 61
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.steps_le_encodedLength line 66
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.value line 72
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.frame line 74
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.joinTrace line 78
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.reindexTrace line 82
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.reindexInTime line 238
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.machine line 257
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.machineInTime line 268
18. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachinePortReindex.lazy_value line 282