OAI/Computability/MinUncut/Machines/Input.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.rowWidth line 25
2. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.rowOffset line 27
3. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.rowsWords_split line 29
4. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.rowsBits_split line 38
5. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.rowsBits_append_split line 47
6. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.prefixWords line 56
7. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.suffixWords line 59
8. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.prefixWords_length line 62
9. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_at_row line 67
10. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableBits_at_row line 76
11. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableBits_header line 82
12. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_row line 87
13. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_take_row line 94
14. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_tail line 100
15. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_reverse line 105
16. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_drop_relation line 110
17. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.relationWords_get line 116
18. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_relation line 121
19. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.tableWords_get_predicate line 131
20. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.rowOffset_lt_length line 138
21. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Input.relationOffset_lt_length line 146
22. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.Alphabet line 168
23. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.Ports line 170
24. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.Label line 172
25. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList line 177
26. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList_getElem?_ctorIdx_eq line 180
27. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList_nodup line 184
28. instance OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.(instance at line 186) line 186
29. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.statement line 190
30. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.resultTapes line 209
31. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.resultTapes_other line 218
32. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.setupInTime line 224
33. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.tableSetupInTime line 314
34. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.program line 341
35. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Setup.machine line 344
36. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.Alphabet line 367
37. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.State line 368
38. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.relationEquiv line 370
39. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.relationFintype line 376
40. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.stateFintype line 379
41. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlot line 384
42. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlot line 394
43. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots line 404
44. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords line 410
45. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots line 413
46. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_preserves_correct line 419
47. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_mem line 431
48. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.fillSlots_finRange line 444
49. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.indexedWords_finRange line 451
50. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readSlots line 463
51. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation line 479
52. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation line 484
53. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.stepAux_readRelation_fromTapes line 495
54. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.readSlots_pushBound line 509
55. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.readRelation_pushBound line 519
56. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.parser line 525
57. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.parser_pushBound line 530
58. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.parserStep line 535
59. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.parserTrace line 549
60. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.ReadRelation.parserInTime line 561
61. def OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.skipWord line 582
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.skipWord_encodeWord line 587
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.skipWord_iterate_encodeWords line 594
64. def OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.headWord line 605
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWord line 610
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWords line 618
67. def OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.lookupBits line 624
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.lookupBits_encodeWords line 627
69. def OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded line 632
70. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.decodeWords_encodeWord line 637
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_encode line 641
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_some line 646
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_none line 651
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.encoded_selected_split line 656
75. def OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.scannedBits line 668
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.encoded_prefix_length_le line 671
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.scannedBits_le line 680
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.scannedBits_of_some line 684
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.selected_scan_length_le line 691
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.output_length_le line 698
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.index_length_le line 705
82. def OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps line 716
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length_strong line 721
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length line 735
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_lt line 740
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_some line 755
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps_add_length_of_invalid line 761
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookupSpec.steps_le_input_encoding_size line 775