OAI/Computability/DirectedFeedback/Machines/MachineAffineLookup.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.Alphabet line 14
2. inductive OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.Label line 16
3. def OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.instruction line 21
4. def OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.steps line 36
5. def OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.finalTapes line 41
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.initialTapes_eq_update line 46
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.affineLookupTrace line 66
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.steps_le line 94
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.steps_le_table line 102
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.finalTapes_other line 109
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.finalTapes_output line 115
12. def OAI.DFVSGames.Foundations.Complexity.MachineAffineLookup.machine line 120
13. abbrev OAI.DFVSGames.Explicit.MachineProductGather.Tape line 142
14. def OAI.DFVSGames.Explicit.MachineProductGather.shift line 144
15. theorem OAI.DFVSGames.Explicit.MachineProductGather.shift_injective line 147
16. def OAI.DFVSGames.Explicit.MachineProductGather.lookupRole line 151
17. theorem OAI.DFVSGames.Explicit.MachineProductGather.lookupRole_injective line 158
18. def OAI.DFVSGames.Explicit.MachineProductGather.Label line 162
19. instance OAI.DFVSGames.Explicit.MachineProductGather.labelFintype line 166
20. instance OAI.DFVSGames.Explicit.MachineProductGather.labelDecidableEq line 173
21. def OAI.DFVSGames.Explicit.MachineProductGather.entry line 180
22. def OAI.DFVSGames.Explicit.MachineProductGather.instruction line 184
23. def OAI.DFVSGames.Explicit.MachineProductGather.steps line 198
24. def OAI.DFVSGames.Explicit.MachineProductGather.finalTapes line 205
25. theorem OAI.DFVSGames.Explicit.MachineProductGather.finalTapes_other line 215
26. theorem OAI.DFVSGames.Explicit.MachineProductGather.gatherTrace line 230
27. theorem OAI.DFVSGames.Explicit.MachineProductGather.finalTapes_field line 290
28. theorem OAI.DFVSGames.Explicit.MachineProductGather.steps_le line 323
29. def OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.guardConfiguration line 351
30. def OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.bodyConfiguration line 357
31. def OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.exitConfiguration line 362
32. def OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.BodyTraces line 367
33. def OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.totalSteps line 376
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.totalSteps_zero line 379
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.totalSteps_succ line 382
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.loopTrace line 387
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.totalSteps_le line 420
38. def OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.loopInTime line 431
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.baseFrame line 452
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.counterFrame line 463
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineCountedLoop.loopTrace_framed line 474
42. inductive OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.Label line 503
43. instance OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.(instance at line 507) line 507
44. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet line 511
45. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.State line 512
46. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.transition line 514
47. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.payload line 515
48. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.emitterLabel line 517
49. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.statement line 520
50. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.program line 537
51. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.machine line 540
52. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes line 551
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_output line 554
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other line 558
55. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.bodySteps line 562
56. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.steps line 563
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.output_encodeWord_inline_MachineUnaryMultiply line 565
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.prepend_payload_inline_MachineUnaryMultiply line 575
59. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.loopBase line 579
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.bodyTrace_inline_MachineUnaryMultiply line 582
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.totalSteps_eq_inline_MachineUnaryMultiply line 640
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.multiplyTrace line 644
63. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime line 718
64. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.timePolynomial line 734
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.steps_le_timePolynomial line 737
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.multiplyFrame line 747
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.programTrace line 751
68. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryMultiply.programInPolynomialTime line 762