OAI/Computability/DirectedFeedback/Machines/MachineCloudPadding.lean

GitHub source file

115 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes line 17
2. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.label line 23
3. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.configuration line 27
4. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.statement line 32
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_apply line 47
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_update line 53
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.stepAux_simulation line 72
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.step_simulation line 99
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Placement.trace line 119
10. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Tape line 136
11. instance OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.(instance at line 140) line 140
12. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Label line 142
13. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.Alphabet line 148
14. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.State line 149
15. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.memory line 151
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.update_count line 164
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.update_scratch line 167
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.update_power line 170
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.update_level line 174
20. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countTape line 178
21. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countView line 186
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countView_left line 195
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countView_right line 197
24. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerTape line 201
25. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerView line 211
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerView_left line 222
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerView_right line 224
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countMemory line 228
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerMemory line 233
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countTapes line 238
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerTapes line 243
32. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.subtractLoop line 250
33. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.program line 258
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.appendTrace_inline_MachineCloudPadding line 273
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.countTrace line 277
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.powerTrace line 293
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.subtractStep_zero line 308
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.subtractStep_succ line 318
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.subtractScanTrace line 328
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.subtractTrace line 351
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.branchStep_zero line 371
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.branchStep_succ line 379
43. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.padding line 388
44. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.postTime line 390
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.postTrace line 393
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.initStep line 421
47. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.totalTime line 428
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingTrace line 432
49. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.inputLength line 453
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.count_length_le line 456
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.table_length_le line 463
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.postTime_le line 468
53. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.timePolynomial line 474
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.totalTime_le line 477
55. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingInTime line 492
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPadding.count_add_padding line 508
57. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.idxOf_map_injective_inline_PreprocessingPaddingOffsets line 520
58. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.sigma_idxOf line 530
59. def OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.offset line 557
60. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.sigma_length line 560
61. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.paddingOrder_val line 566
62. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.vertexOrder_dummy_val line 574
63. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.offset_zero line 581
64. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingPaddingOffsets.offset_all line 584
65. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.Tape line 599
66. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.Label line 604
67. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.Alphabet line 610
68. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.State line 611
69. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.memory line 613
70. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame line 620
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_query line 623
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_count line 625
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_power line 627
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_level line 629
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_bound line 631
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_remaining line 633
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.frame_total line 635
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.update_frame_query line 638
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.update_frame_count line 646
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.update_frame_power line 654
81. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.update_frame_level line 662
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.update_frame_remaining line 670
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.update_frame_total line 674
84. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.paddingView line 679
85. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.paddingView_left line 683
86. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.paddingView_right line 685
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.placedTapes line 689
88. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.program line 696
89. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.appendTrace_inline_MachineCloudPrefix line 712
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.paddingTrace line 716
91. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.incrementStep line 734
92. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.bodyTime line 743
93. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.bodyTrace line 748
94. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.guardStep_succ line 790
95. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.guardStep_zero line 800
96. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.zeroTrace line 808
97. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.amount line 822
98. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.cycleTime line 825
99. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.sumFrom line 828
100. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.loopTime line 832
101. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.loopTrace line 836
102. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_list line 867
103. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_eq_offset line 889
104. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.initStep line 898
105. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.totalTime line 905
106. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.prefixTrace line 908
107. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.cycleBudget line 936
108. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.bodyTime_le line 940
109. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.loopTime_le line 968
110. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.inputLength line 981
111. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.timePolynomial line 984
112. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.totalTime_le line 991
113. def OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.prefixInTime line 1011
114. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.all_padding_sum line 1026
115. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudPrefix.paddingOrder_eq_prefix line 1030