OAI/Computability/MinUncut/Machines/MachineTransducer.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Reduction.MachineTransducer.tapeStacks line 14
2. theorem OAI.MinUncutGames.Reduction.MachineTransducer.update_input line 17
3. theorem OAI.MinUncutGames.Reduction.MachineTransducer.update_output line 22
4. def OAI.MinUncutGames.Reduction.MachineTransducer.output line 29
5. def OAI.MinUncutGames.Reduction.MachineTransducer.loop line 35
6. def OAI.MinUncutGames.Reduction.MachineTransducer.program line 42
7. def OAI.MinUncutGames.Reduction.MachineTransducer.machine line 50
8. def OAI.MinUncutGames.Reduction.MachineTransducer.maxEmission line 62
9. theorem OAI.MinUncutGames.Reduction.MachineTransducer.emission_le line 65
10. theorem OAI.MinUncutGames.Reduction.MachineTransducer.statementPushBound_le line 70
11. theorem OAI.MinUncutGames.Reduction.MachineTransducer.programPushBound_le line 79
12. def OAI.MinUncutGames.Reduction.MachineTransducer.running line 90
13. def OAI.MinUncutGames.Reduction.MachineTransducer.emitting line 95
14. def OAI.MinUncutGames.Reduction.MachineTransducer.halted line 100
15. theorem OAI.MinUncutGames.Reduction.MachineTransducer.step_empty line 104
16. theorem OAI.MinUncutGames.Reduction.MachineTransducer.step_cons line 116
17. theorem OAI.MinUncutGames.Reduction.MachineTransducer.step_emit line 128
18. def OAI.MinUncutGames.Reduction.MachineTransducer.next line 148
19. theorem OAI.MinUncutGames.Reduction.MachineTransducer.two_steps_cons line 153
20. theorem OAI.MinUncutGames.Reduction.MachineTransducer.transduce_steps line 166
21. theorem OAI.MinUncutGames.Reduction.MachineTransducer.initList_eq line 183
22. theorem OAI.MinUncutGames.Reduction.MachineTransducer.haltList_eq line 192
23. theorem OAI.MinUncutGames.Reduction.MachineTransducer.transduce_init_steps line 199
24. def OAI.MinUncutGames.Reduction.MachineTransducer.outputsInTime line 207
25. theorem OAI.MinUncutGames.Reduction.MachineTransducer.outputsInTime_steps line 215
26. def OAI.MinUncutGames.Reduction.MachineTransducer.reversedComputableInPolyTime line 219
27. def OAI.MinUncutGames.Reduction.MachineTransducer.computableInPolyTime line 239
28. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.Alphabet line 258
29. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.State line 259
30. def OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.scanLoop line 261
31. def OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.emitter line 270
32. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.tapes line 276
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.update_source line 280
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.update_scratch line 295
35. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.update_output line 307
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.scanStep_empty line 313
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.scanStep_cons line 331
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.emitterStep line 349
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.twoSteps_cons line 370
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.scanTrace line 396
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.restoreTapes line 430
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyTrace line 449
43. def OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.transduceCopyInTime line 495
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.scanLoop_pushBound line 521
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTransducerCopy.emitter_pushBound line 527
46. inductive OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.Label line 542
47. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList line 546
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_getElem?_ctorIdx_eq line 549
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.Label.enumList_nodup line 553
50. instance OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.(instance at line 555) line 555
51. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.Alphabet line 561
52. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.State line 562
53. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.transition line 564
54. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.payload line 565
55. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.emitterLabel line 567
56. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.statement line 570
57. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.program line 587
58. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.machine line 590
59. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes line 601
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_output line 604
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.resultTapes_other line 608
62. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.bodySteps line 612
63. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.steps line 613
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.output_encodeWord line 615
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.prepend_payload line 625
66. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.loopBase line 629
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.bodyTrace line 632
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.totalSteps_eq line 690
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyTrace line 694
70. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyInTime line 768
71. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.timePolynomial line 784
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.steps_le_timePolynomial line 787
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.multiplyFrame line 797
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.programTrace line 801
75. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryMultiply.programInPolynomialTime line 812