OAI/Computability/MinUncut/Machines/MachineRegularLift.lean

GitHub source file

111 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Lift.statement line 18
2. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Lift.configuration line 24
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Lift.stepAux line 32
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Lift.step line 45
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTable.Lift.trace line 67
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.update_memory_spare line 95
7. inductive OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.RankLabel line 100
8. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankSkip line 106
9. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankProgram line 109
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankProgram_skip line 128
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rowGuard_succ line 133
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rowGuard_zero line 144
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.zeroRowsTrace line 152
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankRowTrace line 166
15. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.prefixTime line 202
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.prefixTrace line 206
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.prefixTime_le line 233
18. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.queryWord line 243
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.encoded_rows_split line 246
20. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankSteps line 254
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankTrace line 259
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.rankSteps_le line 317
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.idxOf_filter_prefix line 330
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.tableRows_length line 349
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.cloudRank_eq_prefix_count line 352
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.cloudRankTrace line 365
27. def OAI.MinUncutGames.Foundations.Complexity.MachineCloudRank.cloudRankInTime line 388
28. inductive OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.Label line 418
29. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.Label.enumList line 423
30. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.Label.enumList_getElem?_ctorIdx_eq line 426
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.Label.enumList_nodup line 430
32. instance OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.(instance at line 432) line 432
33. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.Alphabet line 438
34. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.routine line 440
35. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.fieldBits line 462
36. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.fieldSize line 465
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.fieldBits_length line 469
38. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.prefixTapes line 473
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.prefixTrace line 476
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.appendTrace line 528
41. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.rowBits_eq line 572
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.fieldBits_eq_rowBits line 578
43. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.timePolynomial line 586
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.timePolynomial_bounds line 589
45. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.rowAppendInTime line 596
46. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.machine line 621
47. def OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.machineRowInTime line 632
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableRows.outputFrame line 662
49. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedIndex line 676
50. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow line 681
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_eq line 686
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_tail line 694
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_reverse line 699
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_relation line 712
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.inheritedRow_words line 725
56. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords line 732
57. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.suffixWords line 735
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.prefixWords_length line 738
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_at_row line 743
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.tableWords_drop_row line 755
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.selected_reverse line 761
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.remaining_relation line 768
63. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.Tape line 775
64. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.Buffer line 776
65. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.State line 777
66. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.Alphabet line 778
67. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.zeroBuffer line 780
68. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape line 782
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTape_injective line 784
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.source_outside line 791
71. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.fields line 797
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_zero line 799
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_one line 800
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_two line 801
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.fields_separate line 803
76. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.copyStateEquiv line 806
77. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.Label line 812
78. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopyAt line 818
79. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.instruction line 823
80. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.machine line 835
81. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.looked line 846
82. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.copied line 850
83. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.affined line 855
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.looked_other line 860
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.looked_reverse line 865
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.looked_relation line 869
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.vectorBits_eq_encodedBlock line 879
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.relationBits_eq_encodedBlock line 891
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_step line 895
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.relationCopy_pushBound line 924
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.copied_other line 929
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.copied_reverse line 935
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.copied_relation line 940
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_other line 944
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_reverse line 949
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_relation line 953
97. structure OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.Input line 957
98. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.emittedWords line 966
99. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.affined_fields line 969
100. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.rowSteps line 979
101. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.steps line 982
102. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.finalTapes line 986
103. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.join_trace line 994
104. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.lookupTrace line 998
105. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.copyTrace line 1012
106. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.affineTrace line 1027
107. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.emitTrace line 1048
108. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.traceAt line 1074
109. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.timeBound line 1090
110. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.steps_le line 1093
111. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularOriginalRow.machineInTime line 1110