OAI/Computability/DirectedFeedback/Machines/PoweringMachineRowBody.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.capacity line 58
2. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.bufferSize line 59
3. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.State line 60
4. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.commands line 62
5. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.Label line 65
6. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.planMain line 69
7. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.plan_entry_eq line 76
8. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.entry line 83
9. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement line 86
10. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_output line 91
11. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_other line 96
12. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_injective line 102
13. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.headerPlacement_excludes_data line 118
14. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.instruction line 130
15. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.afterPlan line 141
16. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.rowRelation line 145
17. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.rowWords line 150
18. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit line 155
19. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes line 162
20. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.planSteps line 170
21. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.planSteps_eq line 175
22. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.steps line 188
23. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.Ready line 193
24. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.plan_other_inline_PoweringMachineRowBody line 198
25. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_data line 211
26. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_role line 218
27. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.afterEmit_ready line 228
28. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_data line 250
29. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_ready line 263
30. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_other line 288
31. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.rowBlock_eq_rowRelation line 307
32. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.finalTapes_output line 323
33. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.rowTrace line 352
34. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.budget line 404
35. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.steps_le line 408
36. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRowBody.rowInTime line 419
37. def OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.blockSize line 447
38. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.dartCount_eq_vertex_blocks line 449
39. def OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.blockIndex line 454
40. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.blockIndex_val line 459
41. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.blockIndex_eq_encodeDart line 465
42. def OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRows line 475
43. def OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRowWords line 480
44. def OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRowBits line 484
45. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRows_length line 488
46. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vector_toList_ofFn_inline_PoweringTableLayout line 494
47. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vector_blocks_inline_PoweringTableLayout line 501
48. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.rowList_eq_vertexRows line 517
49. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.outputWords_vertexRows line 523
50. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.encodeWords_flatMap_inline_PoweringTableLayout line 536
51. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.outputBits_vertexRows line 544
52. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRowWords_length line 552
53. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_ge line 559
54. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.vertexRowBits_length_le line 567
55. theorem OAI.DFVSGames.Foundations.PCP.PoweringTableLayout.outputHeader_length line 576
56. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.Command line 593
57. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.ports line 595
58. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.direction line 598
59. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.commands line 601
60. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.commands_length line 603
61. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.LocalLabel line 607
62. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.SequenceLabel line 608
63. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.Label line 609
64. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.State line 610
65. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceEntry line 612
66. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.entry line 617
67. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceInstruction line 620
68. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.instruction line 629
69. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.result line 635
70. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes line 641
71. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.finalTapes line 647
72. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps line 652
73. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.costSum line 658
74. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps_eq line 664
75. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.steps line 677
76. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.budget line 680
77. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.costSum_le line 683
78. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.steps_le line 696
79. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceTrace line 700
80. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.vertexTrace line 730
81. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_ready line 748
82. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_ready line 762
83. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_other line 771
84. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_other line 785
85. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.rowBits line 792
86. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.blockIndex_eq_encodeDart line 796
87. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.rowBits_eq line 803
88. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.encodeWords_flatMap_inline_PoweringMachineVertex line 810
89. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.rows_eq_vertexRowBits line 816
90. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_output line 842
91. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_output line 862
92. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineVertex.vertexInTime line 873