OAI/Combinatorics/IndependentSets/Machines/MachineExpanderRowFrames.lean

GitHub source file

103 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData line 12
2. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.rowData line 19
3. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.control0 line 27
4. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstRow line 28
5. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue line 29
6. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstPair line 30
7. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex line 31
8. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn line 32
9. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.control1 line 33
10. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondRow line 34
11. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue line 35
12. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondPair line 36
13. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex line 37
14. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn line 38
15. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.control2 line 39
16. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.query1 line 40
17. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.query2 line 41
18. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue line 42
19. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.tableLength line 43
20. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_eq_firstRow line 45
21. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_eq_secondRow line 48
22. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_div_degree line 51
23. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_mod_degree line 52
24. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_div_degree line 53
25. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_mod_degree line 54
26. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_eq_residue line 56
27. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_eq_residue line 60
28. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveFirst_residue_eq_control1 line 64
29. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveSecond_residue_eq_control2 line 70
30. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstSelected line 76
31. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondSelected line 80
32. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.evaluateRow_eq line 84
33. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue_eq_step_reverseIndex line 87
34. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.rows_le_tableLength line 94
35. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_le_tableLength line 98
36. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_le_tableLength line 102
37. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_le_tableLength line 106
38. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_le_tableLength line 109
39. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.inputVertex_le_tableLength line 112
40. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex_le_tableLength line 117
41. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex_le_tableLength line 121
42. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_le_tableLength line 125
43. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_le_tableLength line 129
44. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frameContents line 137
45. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame0 line 151
46. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame1 line 153
47. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame2 line 155
48. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3 line 157
49. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame4 line 160
50. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame5 line 162
51. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame6 line 164
52. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame7 line 166
53. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8 line 168
54. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame9 line 171
55. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame10 line 173
56. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame11 line 175
57. def OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame12 line 177
58. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_id_eq line 180
59. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame1_eq line 188
60. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame2_eq line 194
61. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3_eq line 200
62. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame4_eq line 206
63. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame5_eq line 212
64. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame6_eq line 220
65. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame7_eq line 226
66. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8_eq line 233
67. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame9_eq line 240
68. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame10_eq line 247
69. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame11_eq line 255
70. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame12_eq line 263
71. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.final_frame_eq line 269
72. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame0_inputVertex line 274
73. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame0_table line 277
74. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame0_output line 280
75. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame1_inputVertex line 283
76. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame1_emitScratch line 286
77. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame2_queryReverse line 289
78. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame2_queryIndex line 292
79. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3_table line 295
80. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupRestore line 298
81. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupWork line 301
82. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupOutput line 304
83. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame3_queryIndex line 307
84. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame4_lookupOutput line 310
85. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame4_quotientFirst line 313
86. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame4_remainderFirst line 316
87. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame6_quotientFirst line 319
88. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame6_emitScratch line 322
89. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame7_queryReverse line 325
90. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame7_queryIndex line 328
91. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8_table line 331
92. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupRestore line 334
93. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupWork line 337
94. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupOutput line 340
95. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame8_queryIndex line 343
96. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame9_lookupOutput line 346
97. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame9_quotientSecond line 349
98. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame9_remainderSecond line 352
99. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame10_quotientSecond line 355
100. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame10_emitScratch line 358
101. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.frame10_output line 361
102. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.final_dirty_word_length_le line 364
103. theorem OAI.IndependentSetsGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_le_tableLength line 372