OAI/Computability/PerfectCompleteness/Machines/TermMachine.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Tape line 16
2. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Tape.enumList line 21
3. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Tape.enumList_getElem?_ctorIdx_eq line 24
4. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Tape.enumList_nodup line 28
5. instance OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.(instance at line 30) line 30
6. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Alphabet line 34
7. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.State line 35
8. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.initialState line 37
9. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Input line 39
10. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Input.size line 44
11. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.work line 47
12. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Frame line 51
13. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.emitTapes line 57
14. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.emitTapes_reversed line 62
15. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.emitTapes_count line 66
16. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.emitTapes_other line 70
17. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Frame.emit line 75
18. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.tokenBits_append line 87
19. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.emitTapes_append line 91
20. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.emitTapes_count_word line 101
21. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter line 108
22. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.machine line 127
23. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.literalProgram line 138
24. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.literalTrace line 143
25. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.literal line 151
26. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.seqProgram line 162
27. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.seq line 167
28. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.congr line 190
29. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.traceAt line 202
30. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupTapes line 217
31. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupTapes_injective line 224
32. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.LookupLabel line 228
33. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupProgram line 234
34. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupSteps line 245
35. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.trace_trans line 249
36. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupTailTrace line 253
37. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupTrace line 323
38. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.lookupSteps_le line 347
39. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.root line 356
40. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.positionDepth line 369
41. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.position_le line 373
42. structure OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Selector line 381
43. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.compareTape line 396
44. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.compareSlots line 402
45. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.compareSlots_apply line 406
46. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.TestLabel line 408
47. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.testPredicate line 414
48. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.testProgram line 418
49. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.testSteps line 428
50. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.testTrace line 433
51. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.testSteps_le line 475
52. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Selector.positionTest line 488
53. inductive OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.AffineLabel line 498
54. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.affineProgram line 504
55. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.affineAddress line 514
56. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.affineSteps line 517
57. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.affineTrace line 523
58. theorem OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.affineSteps_le line 569
59. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.affineRoot line 589
60. abbrev OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.ChoiceLabel line 609
61. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.choiceProgram line 612
62. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.Emitter.choice line 624
63. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.RootsValid line 686
64. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.termTokens line 689
65. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.compileCell line 693
66. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.compile line 715
67. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.timePolynomial line 739
68. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.termInPolynomialTime line 742
69. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.globalTokens line 757
70. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.compileGlobal line 761
71. def OAI.UniqueGamesTheorem.Foundations.Complexity.CookLevin.TermMachine.globalInLinearTime line 776