OAI/Computability/DirectedFeedback/Machines/MachineCloudCount.lean

GitHub source file

109 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.Tape line 11
2. instance OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.(instance at line 15) line 15
3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.Alphabet line 17
4. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.State line 18
5. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory line 20
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory_original line 28
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory_work line 30
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory_target line 32
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory_scratch line 34
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory_count line 36
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.memory_spare line 38
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.update_memory_work line 41
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.update_memory_target line 45
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.update_memory_scratch line 49
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.update_memory_count line 53
16. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.finishField line 60
17. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.fieldLoop line 63
18. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.hit line 76
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.fieldStep_zero line 78
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_zero line 95
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_succ line 111
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.fieldTrace line 127
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.replicate_encodeWord line 161
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.preservingFieldTrace line 165
25. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.preservingFieldInTime line 197
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.discardFieldsTrace line 217
27. inductive OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.Label line 252
28. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.skipLabel line 257
29. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowEntry line 260
30. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.program line 266
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.program_skip line 279
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowStep_nonempty line 284
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowStep_empty line 294
34. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.Row line 300
35. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowWords line 302
36. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowTime line 304
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowTrace line 307
38. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowsHits line 342
39. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowsTime line 346
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowsTrace line 350
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowTime_le line 374
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowsTime_le line 383
43. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.inputWord line 393
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.inputWord_eq line 396
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.inputWord_length line 400
46. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.totalSteps line 407
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.countTrace line 410
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.totalSteps_le line 445
49. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.tableRows line 454
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.tableRows_width line 458
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.tableRows_words line 464
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.tableRows_input line 471
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowsHits_eq_filter line 476
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowList_eq_finRange_map line 483
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.rowList_cloud_count line 490
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.tableRows_hits line 496
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.cloudCountTrace line 502
58. def OAI.DFVSGames.Foundations.Complexity.MachineCloudCount.cloudCountInTime line 516
59. inductive OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.Tape line 539
60. instance OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.(instance at line 543) line 543
61. inductive OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.Label line 545
62. instance OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.(instance at line 550) line 550
63. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.Alphabet line 552
64. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.State line 553
65. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.memory line 555
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.update_work line 565
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.update_power line 568
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.update_saved line 571
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.update_level line 574
70. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.update_fuel line 577
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.update_product line 580
72. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.compareLoop line 586
73. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.scaleLoop line 596
74. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.program line 605
75. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.overflow line 628
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.compareStep_zero line 630
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_zero line 640
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_succ line 650
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.compareTrace line 660
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.replicate_encodeWord line 685
81. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.compareRestoredTrace line 689
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.appendTrace_inline_MachineCeilingPower line 710
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.scaleStep_succ line 714
84. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.scaleStep_zero line 725
85. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.scaleScanTrace line 735
86. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.scaleTrace line 753
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.cleanupTrace line 775
88. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.guardStep_succ line 786
89. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.guardStep_zero line 797
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.decideStep line 808
91. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.prefixTime line 820
92. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.prefixTrace line 822
93. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.coreTime line 849
94. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.coreTrace line 854
95. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.roundBudget line 882
96. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le line 884
97. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le_roundBudget line 889
98. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.continuingTime_le line 895
99. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.coreTime_le line 903
100. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.initStep line 928
101. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.totalTime line 936
102. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.searchTrace line 938
103. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.timeBound line 958
104. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.totalTime_le line 960
105. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.timePolynomial line 967
106. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.timePolynomial_encoding line 970
107. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.paddingTrace line 974
108. def OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.paddingInTime line 982
109. theorem OAI.DFVSGames.Foundations.Complexity.MachineCeilingPower.paddingOutput_bounds line 993