OAI/Computability/MinUncut/Machines/MachineCloudCount.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Tape line 12
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Tape.enumList line 16
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Tape.enumList_getElem?_ctorIdx_eq line 19
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Tape.enumList_nodup line 23
5. instance OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.(instance at line 25) line 25
6. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Alphabet line 29
7. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.State line 30
8. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory line 32
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory_original line 40
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory_work line 42
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory_target line 44
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory_scratch line 46
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory_count line 48
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.memory_spare line 50
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.update_memory_work line 53
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.update_memory_target line 57
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.update_memory_scratch line 61
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.update_memory_count line 65
19. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.finishField line 72
20. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.fieldLoop line 75
21. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.hit line 88
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.fieldStep_zero line 90
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_zero line 107
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.fieldStep_succ_succ line 123
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.fieldTrace line 139
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.replicate_encodeWord line 173
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.preservingFieldTrace line 177
28. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.preservingFieldInTime line 209
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.discardFieldsTrace line 229
30. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Label line 264
31. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.skipLabel line 269
32. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowEntry line 272
33. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.program line 278
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.program_skip line 291
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowStep_nonempty line 296
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowStep_empty line 306
37. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.Row line 312
38. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowWords line 314
39. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowTime line 316
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowTrace line 319
41. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowsHits line 354
42. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowsTime line 358
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowsTrace line 362
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowTime_le line 386
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowsTime_le line 395
46. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.inputWord line 405
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.inputWord_eq line 408
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.inputWord_length line 412
49. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.totalSteps line 419
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.countTrace line 422
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.totalSteps_le line 457
52. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.tableRows line 466
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.tableRows_width line 470
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.tableRows_words line 476
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.tableRows_input line 483
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowsHits_eq_filter line 488
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowList_eq_finRange_map line 495
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.rowList_cloud_count line 502
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.tableRows_hits line 508
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.cloudCountTrace line 514
61. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudCount.cloudCountInTime line 528
62. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Tape line 553
63. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList line 557
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList_getElem?_ctorIdx_eq line 560
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList_nodup line 564
66. instance OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.(instance at line 566) line 566
67. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Label line 570
68. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Label.enumList line 575
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Label.enumList_getElem?_ctorIdx_eq line 578
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Label.enumList_nodup line 582
71. instance OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.(instance at line 584) line 584
72. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.Alphabet line 588
73. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.State line 589
74. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.memory line 591
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.update_work line 601
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.update_power line 604
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.update_saved line 607
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.update_level line 610
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.update_fuel line 613
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.update_product line 616
81. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.compareLoop line 622
82. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.scaleLoop line 632
83. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.program line 641
84. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.overflow line 664
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.compareStep_zero line 666
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_zero line 676
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_succ line 686
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.compareTrace line 696
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.replicate_encodeWord line 721
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.compareRestoredTrace line 725
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.appendTrace line 746
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.scaleStep_succ line 750
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.scaleStep_zero line 761
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.scaleScanTrace line 771
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.scaleTrace line 789
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.cleanupTrace line 811
97. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.guardStep_succ line 822
98. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.guardStep_zero line 833
99. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.decideStep line 844
100. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.prefixTime line 856
101. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.prefixTrace line 858
102. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.coreTime line 885
103. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.coreTrace line 890
104. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.roundBudget line 918
105. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le line 920
106. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le_roundBudget line 925
107. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.continuingTime_le line 931
108. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.coreTime_le line 939
109. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.initStep line 964
110. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.totalTime line 972
111. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.searchTrace line 974
112. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.timeBound line 994
113. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.totalTime_le line 996
114. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.timePolynomial line 1003
115. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.timePolynomial_encoding line 1006
116. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.paddingTrace line 1010
117. def OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.paddingInTime line 1018
118. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCeilingPower.paddingOutput_bounds line 1029