OAI/Computability/MinUncut/Machines/MachineLookup.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.guard_step_succ line 14
2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.guard_step_zero line 27
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.select_step_nonempty line 40
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.select_step_empty line 56
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.copyTrace line 67
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.selectTrace line 82
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.skipCycleTrace line 97
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.emptyCycleTrace line 115
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.successPrefixTrace line 131
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.lookupTrace_some line 158
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.emptyTrace line 187
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.lookupTrace_invalid line 208
13. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.resultLabel line 230
14. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.resultOutput line 235
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.lookupTrace line 240
16. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.lookupInTime line 262
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.lookupHaltTrace line 278
18. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.timePolynomial line 292
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineLookup.timePolynomial_bounds line 294
20. def OAI.MinUncutGames.Foundations.Complexity.MachineLookup.machineInTime line 302
21. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.Buffer line 324
22. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer line 326
23. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.readSlots line 332
24. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.fill line 341
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.fill_apply line 344
26. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.fill_all line 355
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readSlots line 362
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readAll line 378
29. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_readSlots line 392
30. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.writeSlots line 400
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_writeSlots line 405
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_writeSlots line 420
33. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.blockStmt line 436
34. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.finishAt line 443
35. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt line 448
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockStmt line 452
37. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockMapAt line 459
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockStmt line 467
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockMapAt line 481
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.step_blockMapAt line 492
41. def OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.machine line 509
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineFixedBlockMap.machine_statementPushBound line 520
43. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.Alphabet line 536
44. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.skipBits line 538
45. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits line 549
46. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.stepAux_skipBits_fromTapes line 566
47. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.skipBits_pushBound line 580
48. inductive OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.Label line 588
49. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList line 592
50. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_getElem?_ctorIdx_eq line 595
51. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.Label.enumList_nodup line 599
52. instance OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.(instance at line 601) line 601
53. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.statement line 605
54. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.program line 614
55. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits line 618
56. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.rowBits_eq line 620
57. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits line 625
58. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_nil line 628
59. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.rowsBits_cons line 630
60. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.skipCost line 634
61. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.prefixCost line 637
62. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost line 640
63. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace line 652
64. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.skipRowTrace_fromTapes line 681
65. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.selectTrace line 695
66. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailTrace line 713
67. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.lookupCost_le line 781
68. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.lookupTailInTime line 800
69. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.tableTailTrace line 823
70. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.fullTableTailTrace line 855
71. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.lookup_frame line 895
72. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost line 901
73. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.tableTailCost_le line 905
74. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headIndex line 928
75. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headValue line 931
76. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headValue_eq_semantics line 934
77. abbrev OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.HeadTapes line 937
78. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes line 939
79. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost line 948
80. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupCost_le line 952
81. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headTimePolynomial line 961
82. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupInTime line 964
83. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_head line 1056
84. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.headLookupTapes_frame line 1061
85. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes line 1067
86. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_source line 1072
87. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_tail line 1078
88. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_reverse line 1084
89. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowTapes_frame line 1090
90. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost line 1096
91. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_le line 1099
92. theorem OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowCost_table_le line 1106
93. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.readRowInTime line 1115
94. def OAI.MinUncutGames.Foundations.PCP.AlphabetTable.Lookup.machine line 1199