OAI/Computability/BinPacking/CookLevin/PostfixBounds.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.Tape line 13
2. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.Tape.enumList line 17
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.Tape.enumList_getElem?_ctorIdx_eq line 20
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.Tape.enumList_nodup line 24
5. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.(instance at line 26) line 26
6. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.Alphabet line 30
7. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.State line 31
8. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.Label line 33
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.initialState line 44
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.headerTape line 46
11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.binary line 48
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.readSource line 50
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.readDestination line 52
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.readNext line 55
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.prepare line 58
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.gateTag line 61
17. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldSource line 63
18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldUnused line 67
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldNext line 70
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.resetGoto line 73
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.tagDecoder line 76
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.program line 83
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.machine line 111
24. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.advance line 122
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes line 124
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes_reversed line 127
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes_other line 130
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.outputTapes_twice line 134
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.trace_trans line 141
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.readSource_ne_destination line 145
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldSource_ne_scratch line 150
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldSource_ne_reversed line 155
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.decodeTrace line 160
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.readTrace line 168
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.emitTagTrace line 186
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.FieldReady line 193
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.FieldReady.output line 197
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldSteps line 205
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.fieldTrace line 208
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.rootPushTrace line 244
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.incrementTrace line 256
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.recordSteps line 265
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.recordTrace line 268
44. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.clearTapes line 307
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.clearTrace line 310
46. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.finishTapes line 330
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.finishNodeTrace line 335
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.emitPreparedTrace line 354
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.boundaryTapes line 379
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.preparedTapes line 387
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.operandFields line 397
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.operandSteps line 404
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.tokenSteps line 411
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.tokensSteps line 416
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.argumentBits line 423
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.token_bits line 427
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.prepareInputTrace line 432
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.prepareUnaryTrace line 450
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.prepareBinaryTrace line 468
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.prepareTrace line 499
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.preparedReady line 551
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.tokenTrace line 610
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.tokenBits_cons line 642
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.boundary_remaining line 646
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.guardPositiveTrace line 653
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.tokensTrace line 661
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.initialTapes line 728
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.headersTrace line 735
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.reversedTapes line 775
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.reverseTrace line 779
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.finalTapes line 809
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.compileTrace line 817
73. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixMachine.compileInTime line 846
74. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.RootsBounded line 868
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.TokenBounded line 870
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.fieldSteps_le line 874
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.recordSteps_le line 879
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.gateRecord_slot_le line 887
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.operandSteps_le line 896
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.operandFields_length_le line 902
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.tokenSteps_le line 908
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.takeGate_bounds line 918
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.tokensSteps_le line 964
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.exprTokens_bounded line 992
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.forestTokens_bounded line 1018
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.forest_tokensSteps_le line 1024
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.forest_recordsBits_length_le line 1034
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.forest_phases_le line 1045
89. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.forest_header_le_input_length line 1061
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixBounds.forest_phases_le_input_quadratic line 1068