OAI/Computability/DirectedFeedback/Machines/PoweringMachineLoop.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.HeaderTape line 55
2. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 59) line 59
3. inductive OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.HeaderLabel line 63
4. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.(instance at line 67) line 67
5. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.HeaderAlphabet line 71
6. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.HeaderState line 72
7. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.pushTrue line 74
8. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.stepAux_pushTrue line 79
9. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.pushTrue_pushBound line 91
10. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.headerProgram line 99
11. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.headerMachine line 115
12. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.initialTapes line 126
13. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.scanTapes line 130
14. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.finalTapes line 136
15. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.scanConfiguration line 142
16. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.finalConfiguration line 147
17. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.initializeStep line 151
18. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.scanStep_zero line 161
19. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.scanStep_succ line 172
20. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.scanTrace line 189
21. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.headerTrace line 206
22. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.headerInTime line 218
23. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.remainingRows line 227
24. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_top line 230
25. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.remainingRows_step line 233
26. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.rowBase line 242
27. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.VertexBodyTraces line 246
28. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.vertexBodyTraces_to_counted line 259
29. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime line 272
30. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_output line 295
31. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.varyingRowBase line 301
32. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.VaryingVertexBodyTraces line 305
33. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.varyingVertexBodyTraces_to_counted line 318
34. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.vertexLoopInTime_varying line 331
35. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineLoop.vertexLoop_varying_output line 354
36. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.OtherRegisters line 374
37. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.Master line 375
38. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.CompareState line 376
39. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.RowState line 377
40. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.compareEquiv line 379
41. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.rowEquiv line 382
42. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.compareEquiv_apply line 388
43. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.compareEquiv_symm_apply line 392
44. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.rowEquiv_apply line 396
45. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.rowEquiv_symm_apply line 400
46. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.withBuffer line 404
47. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.clean line 407
48. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.equalityBit_clean line 409
49. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.rowEquiv_withBuffer line 412
50. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.compareEquiv_withBuffer line 415
51. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.clearBuffer line 418
52. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.clearBuffer_apply line 421
53. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.clearBuffer_withBuffer line 426
54. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.encodedBlockAt line 433
55. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.stepAux_encodedBlockAt line 438
56. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.step_encodedBlockAt line 451
57. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.rowAt line 463
58. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.step_rowAt_clean line 468
59. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.rowInTime line 485
60. def OAI.DFVSGames.Foundations.Complexity.PoweringMasterState.headerInTime line 507
61. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.flatMap_word_inline_PortTableLookup line 521
62. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.vertices_word line 553
63. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.darts_word line 556
64. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.row_word_inline_PortTableLookup line 559
65. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.tail_word line 575
66. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.reverse_word line 583
67. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.relation_word line 592
68. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.accepts_word line 604
69. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.rotation_head_word line 611
70. theorem OAI.DFVSGames.Foundations.PCP.PortTableLookup.rotor_lookups line 616
71. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.Alphabet line 637
72. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverseRole line 639
73. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.endpointRole line 642
74. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverseRole_injective line 645
75. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.endpointRole_injective line 646
76. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.source_outside_reverse line 647
77. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverse_outside_endpoint line 648
78. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverseTapes line 650
79. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.endpointTapes line 651
80. inductive OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.Label line 653
81. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.instruction line 658
82. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverseId line 667
83. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverseAddress line 670
84. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.endpointAddress line 673
85. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.reverse_selected line 676
86. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.endpoint_selected line 686
87. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.afterReverse line 692
88. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.finalTapes line 697
89. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.steps line 703
90. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.rotorTrace line 707
91. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_endpoint line 757
92. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_other line 768
93. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.steps_le line 777
94. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRotor.machine line 794