OAI/Computability/MinUncut/Machines/MachineUnaryAdd.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.Alphabet line 13
2. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.finish line 15
3. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.loop line 19
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.loopPushBound line 29
5. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes line 33
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_source line 38
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_destination line 44
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_other line 50
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.update_source line 57
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.update_destination line 70
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_true line 80
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_false line 89
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_succ line 97
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_zero line 108
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.step_succ line 120
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.step_zero line 134
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.addTrace line 148
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.addFromTapes line 172
19. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.addInTime line 192
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryAddAt.addInTime_steps line 210
21. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.Label line 228
22. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.Alphabet line 235
23. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.State line 236
24. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.multiplySlots line 238
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_zero line 241
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_one line 242
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_two line 243
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_three line 244
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.multiplySlots_four line 245
30. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.statement line 249
31. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.program line 261
32. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.machine line 264
33. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.resultTapes line 275
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.resultTapes_output line 278
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.resultTapes_other line 282
36. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.steps line 286
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.radixStepTrace line 288
38. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.radixStepInTime line 372
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.timePolynomial line 390
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.steps_le_timePolynomial line 393
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.programTrace line 404
42. def OAI.MinUncutGames.Foundations.Complexity.MachineRadixStep.programInPolynomialTime line 416
43. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineHorner.Layout line 446
44. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineHorner.Alphabet line 447
45. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineHorner.State line 448
46. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.parity line 450
47. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.accumulator line 454
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.accumulator_ne line 456
49. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixLayout line 459
50. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots line 471
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots_base line 474
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots_acc line 476
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots_digit line 478
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots_out line 480
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots_counter line 482
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radixSlots_scratch line 484
57. inductive OAI.MinUncutGames.Foundations.Complexity.MachineHorner.Label line 487
58. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.entryLabel line 494
59. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.drainLoop line 497
60. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.statement line 506
61. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.program line 520
62. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.machine line 523
63. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.value line 534
64. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.stepCost line 538
65. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.prefixSteps line 541
66. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.stageTapes line 545
67. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.resultTapes line 548
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.drainTrace line 551
69. structure OAI.MinUncutGames.Foundations.Complexity.MachineHorner.Clean line 575
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.Clean.acc line 582
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.digitTrace line 588
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.prefixTrace line 659
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.finishTrace line 680
74. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.steps line 751
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.hornerTrace line 754
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.value_eq_foldl line 785
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.value_add_one_le line 796
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.value_le line 815
79. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.perDigitBound line 823
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.stepCost_le line 827
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.prefixSteps_le line 836
82. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.timePolynomial line 855
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.timePolynomial_eval line 862
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.steps_le_timePolynomial line 868
85. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.hornerInTime line 878
86. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.hornerInPolynomialTime line 894
87. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.operandLength line 914
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.radix_le_operandLength line 918
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.digit_le_operandLength line 925
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.resultTapes_output line 936
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineHorner.resultTapes_other line 940
92. def OAI.MinUncutGames.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime line 944