OAI/Computability/MinUncut/Machines/Alphabet.lean

GitHub source file

106 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.Alphabet line 17
2. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits line 19
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.equalityBits_length_le line 22
4. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits line 25
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_length line 28
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.emittedBits_eq_row line 33
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation line 47
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_div line 54
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selected_rotation_mod line 62
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotationLookupTrace line 70
11. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.FinishLabel line 93
12. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields line 99
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_zero line 103
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_one line 105
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishFields_two line 107
16. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishInstruction line 109
17. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps line 128
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishSteps_le line 133
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.joinTrace line 140
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.finishTrace line 144
21. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.RotorLabel line 259
22. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes line 264
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_injective line 268
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorLookupTapes_outside line 276
25. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorInstruction line 283
26. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorFinalTapes line 294
27. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps line 304
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorTrace line 309
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rotorSteps_le line 388
30. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape line 398
31. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList line 403
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_getElem?_ctorIdx_eq line 406
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectExtraTape.enumList_nodup line 410
34. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 412) line 412
35. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectTape line 416
36. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.RawSelectAlphabet line 417
37. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAlphabet line 419
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectAlphabet_eq line 421
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolWord line 427
40. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes line 432
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.alphabet_tapes_apply line 435
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectToBoolTapes_eq line 442
43. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectState line 450
44. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectStateEquiv line 452
45. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectScratch line 458
46. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectQuery line 459
47. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectOutput line 460
48. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.compareSlots line 462
49. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.subtractSlots line 466
50. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy line 470
51. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList line 474
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_getElem?_ctorIdx_eq line 477
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectCopy.enumList_nodup line 481
54. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 483) line 483
55. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd line 487
56. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList line 491
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_getElem?_ctorIdx_eq line 493
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAdd.enumList_nodup line 497
59. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 499) line 499
60. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage line 503
61. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList line 507
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_getElem?_ctorIdx_eq line 509
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectAddStage.enumList_nodup line 513
64. instance OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.(instance at line 515) line 515
65. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectControl line 519
66. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.SelectLabel line 528
67. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.copySource line 530
68. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.copyDestination line 536
69. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.afterCopy line 542
70. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.addSource line 549
71. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.afterAdd line 553
72. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.cleanupTape line 557
73. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.afterCleanup line 560
74. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectControl line 563
75. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.rawSelectProgram line 585
76. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram line 591
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectProgram_control line 594
78. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanState line 606
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectComparisonTrace line 609
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectCopyTrace line 630
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectAddTrace line 649
82. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.CoreTape line 675
83. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.CoreState line 676
84. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.CoreLabel line 680
85. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.coreEntry line 687
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectCloudTrace line 689
87. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectExtraMemory line 721
88. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory line 734
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_query line 741
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_output line 745
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_scratch line 749
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectMemory_extra line 753
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_query line 758
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_output line 770
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_local line 782
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_size line 794
97. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_left line 806
98. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.update_selectMemory_right line 818
99. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectCleanupTrace line 830
100. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.oldSelectSteps line 873
101. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectOldTrace line 878
102. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps line 922
103. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.dummySelectSteps_eq line 926
104. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectDummyTrace line 931
105. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectionSteps line 990
106. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularInternalRow.selectionTrace line 998