OAI/Combinatorics/IndependentSets/Machines/Basic.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.Extra line 15
2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 19) line 19
3. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.Tape line 23
4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.Alphabet line 24
5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.State line 25
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.tableTape line 27
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.nTape line 28
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.queryTape line 29
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.fuelTape line 30
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.sumTape line 31
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.mTape line 32
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.indexTape line 33
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.workTape line 34
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.scratchTape line 35
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.verticesTape line 36
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.dartsTape line 37
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.emitTape line 38
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.outputTape line 39
19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.memory line 41
20. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame line 53
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_table line 56
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_n line 58
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_query line 60
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_fuel line 62
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_sum line 64
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_m line 66
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_index line 68
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_work line 70
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_scratch line 72
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_vertices line 74
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_darts line 76
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_emit line 78
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.frame_output line 80
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_table line 83
35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_n line 96
36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_query line 109
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_fuel line 122
38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_sum line 135
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_m line 148
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_index line 161
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_work line 174
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_scratch line 187
43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_vertices line 200
44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_darts line 213
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_emit line 226
46. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_output line 239
47. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.Field line 252
48. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 256) line 256
49. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase line 260
50. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 264) line 264
51. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.Label line 268
52. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.fieldTape line 278
53. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.fieldExit line 282
54. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots line 286
55. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots_injective line 289
56. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.copySource line 294
57. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.copyDestination line 299
58. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.copyExit line 303
59. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.prefixView line 308
60. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_left line 312
61. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_right line 314
62. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.prefixTapes line 318
63. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.program line 329
64. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.appendTrace line 359
65. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.paddingTotal line 363
66. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal line 366
67. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.dartTotal line 369
68. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal_eq line 371
69. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.initStep line 376
70. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.seedMStep line 385
71. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.clearIndexStep line 394
72. def OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.readTime line 403
73. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineRegularTable.Header.readTrace line 407