OAI/Computability/MinUncut/Machines/MachineCloudPrefix.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.Tape line 14
2. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.Label line 19
3. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.Alphabet line 25
4. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.State line 26
5. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.memory line 28
6. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame line 35
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_query line 38
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_count line 40
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_power line 42
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_level line 44
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_bound line 46
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_remaining line 48
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.frame_total line 50
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_query line 53
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_count line 61
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_power line 69
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_level line 77
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_remaining line 85
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.update_frame_total line 89
20. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.paddingView line 94
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.paddingView_left line 98
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.paddingView_right line 100
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.placedTapes line 104
24. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.program line 111
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.appendTrace line 127
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.paddingTrace line 131
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.incrementStep line 149
28. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.bodyTime line 158
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.bodyTrace line 163
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.guardStep_succ line 205
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.guardStep_zero line 215
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.zeroTrace line 223
33. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.amount line 237
34. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.cycleTime line 240
35. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom line 243
36. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.loopTime line 247
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.loopTrace line 251
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_list line 282
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_eq_offset line 301
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.initStep line 310
41. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.totalTime line 317
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.prefixTrace line 320
43. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.cycleBudget line 348
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.bodyTime_le line 352
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.loopTime_le line 380
46. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.inputLength line 393
47. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.timePolynomial line 396
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.totalTime_le line 403
49. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.prefixInTime line 423
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.all_padding_sum line 438
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudPrefix.paddingOrder_eq_prefix line 442
52. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet line 458
53. inductive OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.Label line 460
54. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.statement line 465
55. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.program line 471
56. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.steps line 475
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.remaining_length_le line 479
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le line 486
59. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.timePolynomial line 494
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le_timePolynomial line 496
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt line 502
62. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt line 558
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.initialTapes_eq line 579
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt_fromTapes line 588
65. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.machine line 609
66. def OAI.MinUncutGames.Foundations.Complexity.MachinePreservingLookupClean.machineInTime line 620
67. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.Alphabet line 642
68. def OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendTapes line 644
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendTapes_source line 648
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendTapes_destination line 653
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendTapes_other line 657
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendTapes_scratch line 662
73. def OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.firstTapes line 669
74. def OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.secondTapes line 672
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.finalTapes_eq line 676
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendTrace line 698
77. def OAI.MinUncutGames.Foundations.Complexity.MachineAppendAt.appendInTime line 768