OAI/Computability/MinUncut/Machines/PoweringMachineVertex.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.Command line 13
2. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.ports line 15
3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.direction line 18
4. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.commands line 21
5. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.commands_length line 23
6. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.LocalLabel line 27
7. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.SequenceLabel line 28
8. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.Label line 29
9. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.State line 30
10. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceEntry line 32
11. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.entry line 37
12. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceInstruction line 40
13. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.instruction line 49
14. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.result line 55
15. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes line 61
16. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes line 67
17. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps line 72
18. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.costSum line 78
19. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps_eq line 84
20. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.steps line 97
21. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.budget line 100
22. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.costSum_le line 103
23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.steps_le line 116
24. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTrace line 120
25. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.vertexTrace line 150
26. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_ready line 168
27. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_ready line 182
28. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_other line 191
29. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_other line 205
30. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.rowBits line 212
31. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.blockIndex_eq_encodeDart line 216
32. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.rowBits_eq line 224
33. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.encodeWords_flatMap line 231
34. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.rows_eq_vertexRowBits line 237
35. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_output line 260
36. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_output line 280
37. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineVertex.vertexInTime line 291
38. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.Placement line 317
39. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.State line 318
40. structure OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.Ready line 320
41. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.counter line 328
42. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.counter_other line 331
43. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_vertex line 338
44. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_of_vertex line 357
45. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexStart line 363
46. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexEntry line 366
47. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.bridge line 384
48. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes line 388
49. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.steps line 396
50. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.steps_le line 402
51. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_ready line 414
52. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows line 439
53. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_ofFn line 444
54. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_all line 461
55. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_output line 468
56. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_other line 494
57. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.loopTrace line 506
58. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineOuterLoop.loopInTime line 572
59. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.Alphabet line 603
60. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.Label line 605
61. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.copyInstruction line 609
62. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.instruction line 616
63. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.program line 628
64. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.afterD line 633
65. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders line 636
66. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_output line 639
67. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_other line 643
68. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.copySteps line 647
69. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.copySteps_eq line 649
70. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.steps line 653
71. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.budget line 657
72. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.trace_trans line 661
73. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.traceAt line 665
74. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.trace line 714
75. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.steps_le_budget line 730
76. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.afterHeaders_length_le line 736
77. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.steps_le_uniform line 749
78. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineFinish.execution line 763