OAI/Combinatorics/IndependentSets/Machines/SelectAlphabet.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectAlphabet line 15
2. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectAlphabet_eq line 17
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolWord line 23
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes line 28
5. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.alphabet_tapes_apply line 31
6. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes_eq line 38
7. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectState line 46
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectStateEquiv line 48
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch line 54
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectQuery line 55
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectOutput line 56
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.compareSlots line 58
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.subtractSlots line 62
14. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy line 66
15. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 70) line 70
16. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd line 74
17. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 78) line 78
18. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage line 82
19. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 85) line 85
20. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectControl line 89
21. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.SelectLabel line 98
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.copySource line 100
23. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.copyDestination line 106
24. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.afterCopy line 112
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.addSource line 119
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.afterAdd line 123
27. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.cleanupTape line 127
28. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.afterCleanup line 130
29. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectControl line 133
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.rawSelectProgram line 155
31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram line 161
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram_control line 164
33. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState line 176
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectComparisonTrace line 179
35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectCopyTrace line 200
36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectAddTrace line 219
37. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape line 245
38. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.CoreState line 246
39. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel line 250
40. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry line 257
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectCloudTrace line 259
42. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectExtraMemory line 291
43. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory line 304
44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_query line 311
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_output line 315
46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_scratch line 319
47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_extra line 323
48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_query line 328
49. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_output line 340
50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_local line 352
51. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_size line 364
52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_left line 376
53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_right line 388
54. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanupTrace line 400