OAI/Combinatorics/IndependentSets/Machines/MachineInitialHeaders.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.Alphabet line 17
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixScan line 19
3. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.update_source line 30
4. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.update_scratch line 44
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.update_output line 55
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_true line 61
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixStep_false line 72
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.replicate_append_cons line 82
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixScanTrace line 87
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixTrace line 124
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixInTime line 174
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.prefixScan_pushBound line 193
13. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.literalTrace line 200
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.trace_trans line 213
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.headerTrace line 217
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineInitialHeaders.headerInTime line 297