OAI/Computability/DirectedFeedback/Machines/MachineUnaryAdd.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.Alphabet line 14
2. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.finish line 16
3. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.loop line 20
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.loopPushBound line 30
5. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes line 34
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_source line 39
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_destination line 45
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_other line 51
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.update_source_inline_MachineUnaryAddAt line 58
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.update_destination_inline_MachineUnaryAddAt line 71
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_true line 81
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_false line 90
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_succ line 98
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_zero line 109
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.step_succ line 121
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.step_zero line 135
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.addTrace line 149
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.addFromTapes line 173
19. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.addInTime line 193
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryAddAt.addInTime_steps line 211
21. inductive OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.Label line 232
22. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.Alphabet line 237
23. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.State line 238
24. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.multiplySlots line 240
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.multiplySlots_zero line 243
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.multiplySlots_one line 244
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.multiplySlots_two line 245
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.multiplySlots_three line 246
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.multiplySlots_four line 247
30. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.statement line 251
31. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.program line 263
32. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.machine line 266
33. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.resultTapes line 277
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.resultTapes_output line 280
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.resultTapes_other line 284
36. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.steps line 288
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.radixStepTrace line 290
38. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.radixStepInTime line 374
39. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.timePolynomial line 392
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.steps_le_timePolynomial line 395
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.programTrace line 406
42. def OAI.DFVSGames.Foundations.Complexity.MachineRadixStep.programInPolynomialTime line 418
43. abbrev OAI.DFVSGames.Foundations.Complexity.MachineHorner.Layout line 449
44. abbrev OAI.DFVSGames.Foundations.Complexity.MachineHorner.Alphabet line 450
45. abbrev OAI.DFVSGames.Foundations.Complexity.MachineHorner.State line 451
46. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.parity line 453
47. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.accumulator line 457
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.accumulator_ne line 459
49. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixLayout line 462
50. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots line 474
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots_base line 477
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots_acc line 479
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots_digit line 481
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots_out line 483
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots_counter line 485
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radixSlots_scratch line 487
57. inductive OAI.DFVSGames.Foundations.Complexity.MachineHorner.Label line 490
58. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.entryLabel line 497
59. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.drainLoop line 500
60. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.statement line 509
61. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.program line 523
62. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.machine line 526
63. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.value line 537
64. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.stepCost line 541
65. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.prefixSteps line 544
66. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.stageTapes line 548
67. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.resultTapes line 551
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.drainTrace line 554
69. structure OAI.DFVSGames.Foundations.Complexity.MachineHorner.Clean line 578
70. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.Clean.acc line 585
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.digitTrace line 591
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.prefixTrace line 662
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.finishTrace line 683
74. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.steps line 754
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.hornerTrace line 757
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.value_eq_foldl line 788
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.value_add_one_le line 799
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.value_le line 818
79. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.perDigitBound line 826
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.stepCost_le line 830
81. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.prefixSteps_le line 839
82. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.timePolynomial line 858
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.timePolynomial_eval line 865
84. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.steps_le_timePolynomial line 871
85. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.hornerInTime line 881
86. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.hornerInPolynomialTime line 897
87. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.operandLength line 917
88. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.radix_le_operandLength line 921
89. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.digit_le_operandLength line 928
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.resultTapes_output line 939
91. theorem OAI.DFVSGames.Foundations.Complexity.MachineHorner.resultTapes_other line 943
92. def OAI.DFVSGames.Foundations.Complexity.MachineHorner.hornerInEncodedPolynomialTime line 947