OAI/Computability/BinPacking/CookLevin/CircuitProducer.lean

GitHub source file

66 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.drainStep_cons line 12
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.drainStep_nil line 24
3. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.drainTrace line 35
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.drainTrace_base line 54
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.drainInTime line 63
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.tagStep line 74
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.tagInTime line 83
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.clearFields line 93
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.clearFields_field line 97
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.clearFields_other line 101
11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.cleanupSteps line 105
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.cleanupTrace line 109
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.cleanupInTime line 131
14. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.finishTapes line 141
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.counterStep line 146
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.finishTrace line 151
17. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerStages.finishInTime line 181
18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerHeaders.parsedTapes line 198
19. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerHeaders.resultTapes line 206
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerHeaders.parsedTapes_eq line 215
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerHeaders.headersTrace line 226
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerHeaders.headersInTime line 297
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordsInput line 317
24. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordsOutput line 318
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.tapes line 320
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.parsedFields line 329
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.decodedFields line 330
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.update_reversed line 333
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.counterTapes_eq line 340
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.fourTapes_eq line 348
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.decodeTapes_eq line 363
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.clearFields_eq line 372
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.cleanupSteps_eq line 381
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordBits_length line 388
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.bodyCost line 393
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.bodyInTime line 397
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.loopCost line 439
38. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.loopInTime line 443
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.bodyCost_le line 475
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.loopCost_le line 481
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordOutput_length_le line 491
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerLoop.recordsOutput_length_le line 496
43. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.Input line 512
44. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.inputBits line 517
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.outputHeaders line 520
46. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.producedBits line 523
47. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.inputTapes line 526
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.retainedTapes line 529
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.guardTapes line 532
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.afterLoopTapes line 536
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.beforeFinishTapes line 540
52. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.initList_eq line 543
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.headers_result_eq line 553
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.output_result_eq line 560
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.finish_eq line 567
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.inputBits_length line 577
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.producedBits_length_le line 583
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.fullRunInTime line 591
59. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducerRuntime.computableInPolyTime line 632
60. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.asInput line 656
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.recordsInput_eq line 659
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.recordsOutput_eq line 668
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.inputBits_asInput line 677
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.producedBits_asInput line 682
65. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.fullRunInTime line 688
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitProducer.computableInPolyTime line 694