OAI/Combinatorics/IndependentSets/Machines/MachineVertexPadding.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.Tape line 13
2. instance OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.(instance at line 18) line 18
3. inductive OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.Label line 23
4. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.Alphabet line 32
5. abbrev OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.State line 33
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.memory line 35
7. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.update_output line 46
8. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.update_vertex line 49
9. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.update_edge line 52
10. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.update_power line 55
11. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.update_fuel line 58
12. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.update_relation line 61
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitTape line 65
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitView line 66
15. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitView_left line 74
16. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitView_right line 76
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.powerTape line 80
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.powerView line 89
19. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.powerView_left line 100
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.powerView_right line 102
21. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.subtractTape line 106
22. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.subtractView line 117
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.subtractView_left line 130
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.subtractView_right line 132
25. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowTape line 136
26. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowView line 139
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowView_left line 149
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowView_right line 153
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowAlphabet_eq line 159
30. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowStateEquiv line 162
31. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowProgram line 168
32. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.program line 175
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.appendTrace line 201
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.tableBits_split line 205
35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitInitialTapes line 211
36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitResultTapes line 217
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.splitTrace line 223
38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.powerTapes line 240
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.powerTrace line 245
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.affineTapes line 259
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.affineOutputTrace line 266
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.headersTrace line 308
43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.copyPowerTrace line 324
44. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.subtractTapes line 338
45. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.subtractTrace line 345
46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowBoolTapes line 360
47. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.transport_tapes_apply line 365
48. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowCastTapes line 372
49. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowInitialTapes line 378
50. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowFinalTapes line 385
51. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowTime line 393
52. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.frameTrace line 396
53. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rowsTrace line 405
54. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.cleanupTime line 439
55. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.cleanupTrace line 441
56. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.otherTime line 476
57. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.totalTime line 483
58. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingTrace line 486
59. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.rows_length_le line 522
60. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.darts_length_le line 527
61. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.power_length_bound line 531
62. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.initialOutput_length line 536
63. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.intermediateCoefficient line 543
64. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.intermediatePolynomial line 545
65. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.intermediate_bound line 548
66. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.otherPolynomial line 563
67. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.otherTime_le line 567
68. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.timePolynomial line 583
69. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.totalTime_le line 586
70. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingInTime line 597
71. def OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.machine line 611
72. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineVertexPadding.alphabet_finite line 622