OAI/Combinatorics/IndependentSets/Machines/ProfileMachine.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.setEntry line 9
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.setEntry_apply line 12
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.setExpected line 18
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.foldProfile line 22
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.foldProfile_apply line 25
6. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.Tape line 41
7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.Label line 42
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.labelAt line 44
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.storePair line 47
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.profileProgram line 52
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.pairTime line 72
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.prefixProfile line 76
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.prefixTime line 80
14. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.prefixProfile_succ line 84
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.prefixTime_succ line 92
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.stageInTime line 99
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.prefixInTime line 144
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.allPairs line 164
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.mem_allPairs line 167
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.length_allPairs line 170
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.foldProfile_allPairs line 173
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.profileMachine line 178
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.profileInTime line 189
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.pairTime_le line 215
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.totalTime_le line 224
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineFieldProfile.profileInTime_bounded line 234