OAI/Computability/DirectedFeedback/Machines/MachineRegularInternalRow.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet line 60
2. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits line 62
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits_length_le line 65
4. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits line 68
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_length line 71
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_eq_row line 76
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation line 90
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_div line 97
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_mod line 105
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotationLookupTrace line 113
11. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel line 136
12. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishFields line 142
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_zero line 146
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_one line 148
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_two line 150
16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction line 152
17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps line 171
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps_le line 176
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.joinTrace_inline_MachineRegularInternalRow line 183
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.finishTrace line 187
21. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.RotorLabel line 302
22. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes line 307
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_injective line 311
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_outside line 319
25. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction line 326
26. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorFinalTapes line 337
27. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps line 347
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorTrace line 352
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps_le line 431
30. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape line 441
31. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 446) line 446
32. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape line 448
33. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet line 449
34. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectAlphabet line 451
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectAlphabet_eq line 453
36. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolWord line 459
37. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes line 464
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.alphabet_tapes_apply_inline_MachineRegularInternalRow line 467
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes_eq line 474
40. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectState line 482
41. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectStateEquiv line 484
42. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch line 490
43. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectQuery line 491
44. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectOutput line 492
45. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.compareSlots line 494
46. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.subtractSlots line 498
47. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy line 502
48. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 506) line 506
49. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd line 508
50. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 512) line 512
51. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage line 514
52. instance OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 517) line 517
53. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectControl line 519
54. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.SelectLabel line 528
55. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.copySource line 530
56. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.copyDestination line 536
57. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.afterCopy line 542
58. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.addSource line 549
59. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.afterAdd line 553
60. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.cleanupTape line 557
61. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.afterCleanup line 560
62. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectControl line 563
63. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.rawSelectProgram line 585
64. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram line 591
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram_control line 594
66. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState line 606
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectComparisonTrace line 609
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectCopyTrace line 630
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectAddTrace line 649
70. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape line 675
71. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.CoreState line 676
72. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel line 680
73. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry line 687
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectCloudTrace line 689
75. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectExtraMemory line 721
76. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory line 734
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_query line 741
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_output line 745
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_scratch line 749
80. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_extra line 753
81. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_query line 758
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_output line 770
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_local line 782
84. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_size line 794
85. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_left line 806
86. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_right line 818
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanupTrace line 830
88. def OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.oldSelectSteps line 873
89. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularInternalRow.selectOldTrace line 878