OAI/Computability/BinPacking/Computation/MachineHorner.lean

GitHub source file

120 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.Alphabet line 17
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.State line 18
3. def OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.scanLoop line 20
4. def OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.emitter line 29
5. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.tapes line 35
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.update_source line 39
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.update_scratch line 54
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.update_output line 66
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.scanStep_empty line 72
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.scanStep_cons line 90
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.emitterStep line 108
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.twoSteps_cons line 129
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.scanTrace line 155
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.restoreTapes line 189
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyTrace line 208
16. def OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyInTime line 254
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.scanLoop_pushBound line 280
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTransducerCopy.emitter_pushBound line 286
19. inductive OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.Label line 299
20. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList line 303
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_getElem?_ctorIdx_eq line 306
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_nodup line 310
23. instance OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.(instance at line 312) line 312
24. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet line 318
25. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.State line 319
26. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.transition line 321
27. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.payload line 322
28. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.emitterLabel line 324
29. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.statement line 327
30. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.program line 344
31. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.machine line 347
32. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes line 358
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_output line 361
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other line 365
35. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.bodySteps line 369
36. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.steps line 370
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.output_encodeWord line 372
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.prepend_payload line 382
39. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.loopBase line 386
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.bodyTrace line 389
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.totalSteps_eq line 447
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.multiplyTrace line 451
43. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime line 525
44. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.timePolynomial line 541
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.steps_le_timePolynomial line 544
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.multiplyFrame line 554
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.programTrace line 558
48. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryMultiply.programInPolynomialTime line 569
49. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.Label line 593
50. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.Alphabet line 600
51. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.State line 601
52. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.multiplySlots line 603
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.multiplySlots_zero line 606
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.multiplySlots_one line 607
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.multiplySlots_two line 608
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.multiplySlots_three line 609
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.multiplySlots_four line 610
58. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.statement line 614
59. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.program line 626
60. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.machine line 629
61. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.resultTapes line 640
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.resultTapes_output line 643
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.resultTapes_other line 647
64. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.steps line 651
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.radixStepTrace line 653
66. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.radixStepInTime line 737
67. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.timePolynomial line 755
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.steps_le_timePolynomial line 758
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.programTrace line 769
70. def OAI.BinPackingGames.Foundations.Complexity.MachineRadixStep.programInPolynomialTime line 781
71. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineHorner.Layout line 811
72. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineHorner.Alphabet line 812
73. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineHorner.State line 813
74. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.parity line 815
75. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.accumulator line 819
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.accumulator_ne line 821
77. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixLayout line 824
78. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots line 836
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots_base line 839
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots_acc line 841
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots_digit line 843
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots_out line 845
83. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots_counter line 847
84. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radixSlots_scratch line 849
85. inductive OAI.BinPackingGames.Foundations.Complexity.MachineHorner.Label line 852
86. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.entryLabel line 859
87. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.drainLoop line 862
88. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.statement line 871
89. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.program line 885
90. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.machine line 888
91. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.value line 899
92. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.stepCost line 903
93. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.prefixSteps line 906
94. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.stageTapes line 910
95. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.resultTapes line 913
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.drainTrace line 916
97. structure OAI.BinPackingGames.Foundations.Complexity.MachineHorner.Clean line 940
98. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.Clean.acc line 947
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.digitTrace line 953
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.prefixTrace line 1024
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.finishTrace line 1045
102. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.steps line 1116
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.hornerTrace line 1119
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.value_eq_foldl line 1150
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.value_add_one_le line 1161
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.value_le line 1180
107. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.perDigitBound line 1188
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.stepCost_le line 1192
109. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.prefixSteps_le line 1201
110. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.timePolynomial line 1220
111. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.timePolynomial_eval line 1227
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.steps_le_timePolynomial line 1233
113. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.hornerInTime line 1243
114. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.hornerInPolynomialTime line 1259
115. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.operandLength line 1279
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.radix_le_operandLength line 1283
117. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.digit_le_operandLength line 1290
118. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.resultTapes_output line 1301
119. theorem OAI.BinPackingGames.Foundations.Complexity.MachineHorner.resultTapes_other line 1305
120. def OAI.BinPackingGames.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime line 1309