OAI/Computability/DirectedFeedback/Machines/MachineLookupSpec.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.skipWord line 9
2. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.skipWord_encodeWord line 14
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.skipWord_iterate_encodeWords line 21
4. def OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.headWord line 32
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWord line 37
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.headWord_encodeWords line 45
7. def OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.lookupBits line 51
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.lookupBits_encodeWords line 54
9. def OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded line 59
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.decodeWords_encodeWord line 64
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_encode line 68
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_some line 73
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.lookupEncoded_none line 78
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.encoded_selected_split line 83
15. def OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.scannedBits line 95
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.encoded_prefix_length_le line 98
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.scannedBits_le line 107
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.scannedBits_of_some line 111
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.selected_scan_length_le line 118
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.output_length_le line 125
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.index_length_le line 132
22. def OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps line 143
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length_strong line 148
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps_le_encoded_length line 162
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_lt line 167
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps_eq_scannedBits_of_some line 182
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps_add_length_of_invalid line 188
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookupSpec.steps_le_input_encoding_size line 202
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.discard_update_twice_inline_MachineLookupDiscard line 217
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.discardStep_delimiter line 226
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.discardStep_true line 239
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.discard_empty_step line 252
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.discardTrace_update line 268
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.discardTrace line 291
35. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.discardInTime line 310
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.guard_step_succ line 335
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.guard_step_zero line 348
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.select_step_nonempty line 361
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.select_step_empty line 377
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.copyTrace line 388
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.selectTrace line 403
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.skipCycleTrace line 418
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.emptyCycleTrace line 436
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.successPrefixTrace line 452
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.lookupTrace_some line 479
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.emptyTrace line 508
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.lookupTrace_invalid line 529
48. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.resultLabel line 551
49. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.resultOutput line 556
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.lookupTrace line 561
51. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.lookupInTime line 583
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.lookupHaltTrace line 599
53. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.timePolynomial line 613
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineLookup.timePolynomial_bounds line 615
55. def OAI.DFVSGames.Foundations.Complexity.MachineLookup.machineInTime line 623
56. def OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.label line 646
57. def OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.configuration line 650
58. def OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.statement line 653
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.stepAux_simulation line 667
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.step_simulation line 688
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.trace line 704
62. def OAI.DFVSGames.Foundations.Complexity.MachineSubroutine.execution line 714
63. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.Alphabet line 734
64. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.initialTapes line 736
65. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.finalTapes line 741
66. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.lookupFramedHaltTrace_some line 748
67. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupTrace line 766
68. theorem OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.preservingLookup_steps_le line 816
69. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupInTime line 824
70. inductive OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.Label line 846
71. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.program line 850
72. def OAI.DFVSGames.Foundations.Complexity.MachinePreservingLookup.machine line 857