OAI/Computability/BinPacking/CookLevin/TermMachine.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Tape line 12
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Tape.enumList line 17
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Tape.enumList_getElem?_ctorIdx_eq line 20
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Tape.enumList_nodup line 24
5. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.(instance at line 26) line 26
6. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Alphabet line 30
7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.State line 31
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.initialState line 33
9. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Input line 35
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Input.size line 40
11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.work line 43
12. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Frame line 47
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.emitTapes line 53
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.emitTapes_reversed line 58
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.emitTapes_count line 62
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.emitTapes_other line 66
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Frame.emit line 71
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.tokenBits_append line 83
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.emitTapes_append line 87
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.emitTapes_count_word line 97
21. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter line 104
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.machine line 123
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.literalProgram line 134
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.literalTrace line 139
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.literal line 147
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.seqProgram line 158
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.seq line 163
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.congr line 186
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.traceAt line 198
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupTapes line 213
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupTapes_injective line 220
32. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.LookupLabel line 224
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupProgram line 230
34. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupSteps line 241
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.trace_trans line 245
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupTailTrace line 249
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupTrace line 319
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.lookupSteps_le line 343
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.root line 352
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.positionDepth line 365
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.position_le line 369
42. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Selector line 377
43. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.compareTape line 392
44. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.compareSlots line 398
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.compareSlots_apply line 402
46. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.TestLabel line 404
47. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.testPredicate line 410
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.testProgram line 414
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.testSteps line 424
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.testTrace line 429
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.testSteps_le line 471
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Selector.positionTest line 484
53. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.AffineLabel line 494
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.affineProgram line 500
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.affineAddress line 510
56. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.affineSteps line 513
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.affineTrace line 519
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.affineSteps_le line 565
59. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.affineRoot line 585
60. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.ChoiceLabel line 605
61. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.choiceProgram line 608
62. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.Emitter.choice line 620
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.RootsValid line 681
64. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.termTokens line 684
65. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.compileCell line 688
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.compile line 710
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.timePolynomial line 734
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.termInPolynomialTime line 737
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.globalTokens line 752
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.compileGlobal line 756
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TermMachine.globalInLinearTime line 771