OAI/Computability/PerfectCompleteness/Machines/ProducerBootstrapLemmas.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.Ports line 18
2. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.Label line 20
3. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.Label.enumList line 24
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.Label.enumList_getElem?_ctorIdx_eq line 26
5. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.Label.enumList_nodup line 30
6. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.(instance at line 32) line 32
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.State line 36
8. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.Ready line 38
9. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.copied line 45
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared line 48
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.statement line 52
12. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_current line 61
13. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_source line 65
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_count line 69
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_cursor line 73
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_scratch line 77
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.prepared_other line 81
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.seedTrace line 85
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.trace line 98
20. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.ProducerBootstrap.inTime line 119
21. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.Alphabet line 145
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.guard line 147
23. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.guardStep_nil line 155
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.guardStep_nonempty line 166
25. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.fieldTapes_overwrite line 179
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.steps line 193
27. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.steps_nil line 195
28. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.steps_cons line 197
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.steps_le_length line 202
30. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.refreshTrace line 208
31. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.refreshInTime line 264
32. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.refresh_other line 286
33. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.Label line 292
34. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.Label.enumList line 296
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.Label.enumList_getElem?_ctorIdx_eq line 298
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.Label.enumList_nodup line 302
37. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.(instance at line 304) line 304
38. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.program line 308
39. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.machine line 314
40. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.machineTrace line 325
41. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.RootRefresh.computableInPolyTime line 343
42. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.Cells line 367
43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode line 369
44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.read line 371
45. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.head line 374
46. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.isEmpty line 376
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.popShift line 378
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.pushShift line 381
49. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode_apply line 384
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode_nil line 387
51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.read_at line 391
52. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.read_of_capacity_le line 395
53. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.read_encode line 399
54. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.head_encode line 406
55. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.head_encode_eq_none_iff line 410
56. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.isEmpty_encode line 414
57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.isEmpty_encode_eq_true_iff line 419
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode_tail line 424
59. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode_cons line 430
60. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.tail_length_le line 435
61. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.cons_length_le line 440
62. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode_injective line 445
63. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encode_eq_iff line 452
64. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.BoundedStack line 457
65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.boundedEncoding line 459
66. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.boundedPop line 466
67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.boundedPush line 469
68. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.boundedPop_correct line 473
69. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.boundedPush_correct line 477
70. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes line 486
71. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_update line 489
72. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_pop line 498
73. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_push line 504
74. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_injective line 511