OAI/Computability/MinUncut/Machines/Addresses.lean

GitHub source file

96 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.Terms line 11
2. structure OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.Field line 13
3. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.values line 17
4. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.eval line 19
5. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound line 22
6. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound_pos line 25
7. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.tapeCount_lt_bound line 29
8. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.pairTapeCount_lt_bound line 33
9. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.localCount_lt_bound line 37
10. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.local_add_pair_lt_bound line 41
11. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.twelve_local_lt_bound line 45
12. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.zeroOffset line 49
13. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.eventOffset line 51
14. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryOffset line 55
15. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.reverseOffset line 61
16. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices line 71
17. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts line 74
18. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField line 77
19. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.vertexQueryTerms line 81
20. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.edgeQueryTerms line 84
21. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms line 87
22. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField line 91
23. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField line 94
24. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_eval line 98
25. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_eval line 104
26. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_eval line 109
27. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField_eval line 116
28. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_eval line 132
29. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms line 142
30. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_query line 146
31. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventOffset line 154
32. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent line 158
33. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eq_rawQueryField line 162
34. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval line 169
35. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval_verifier line 178
36. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms line 187
37. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailOffset line 191
38. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail line 195
39. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail_eval line 199
40. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.CoefficientsBounded line 211
41. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_coefficients line 214
42. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_coefficients line 221
43. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_coefficients line 227
44. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_coefficients line 234
45. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_coefficients line 252
46. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_coefficients line 256
47. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_length_le line 264
48. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_length_le line 270
49. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_coefficients line 274
50. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_length_le line 281
51. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Addresses.offset_lt line 288
52. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.Context line 299
53. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand line 300
54. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits line 302
55. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.vector_list_ofFn line 307
56. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.bitValues_ofFn line 312
57. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits_values line 321
58. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands line 329
59. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.rowContext line 338
60. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues line 342
61. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.encodedRow line 348
62. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_bits line 354
63. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands line 385
64. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockWords line 390
65. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.tableWords_eq_blocks line 397
66. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands line 408
67. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_bits line 414
68. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_length line 428
69. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.headerInTime line 432
70. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.encodeWords_flatMap line 457
71. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_bits line 463
72. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_length_le line 470
73. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.flatMap_length_le line 478
74. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_length_le line 489
75. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTime line 500
76. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn line 529
77. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn_bits line 533
78. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTimeAmbient line 542
79. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.Alphabet line 582
80. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.finish line 584
81. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction line 589
82. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_drain line 598
83. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.instruction_finish line 606
84. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes line 611
85. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost line 616
86. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_apply line 622
87. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_selected line 635
88. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_unselected line 639
89. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.actualCost_le line 645
90. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupTrace line 661
91. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.cleanupInTime line 686
92. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.program line 702
93. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.machine line 706
94. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.machineInTime line 718
95. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.clearTapes_outputOnly line 729
96. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Cleanup.machineHaltInTime line 741