OAI/Computability/BinPacking/CookLevin/TransitionArena.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.Snapshot line 12
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_ext line 18
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot line 26
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.next line 31
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.rootValues line 32
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.recordBits line 33
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.Snapshot.currentBits line 36
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.Snapshot.rootBits line 37
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.lowerStage line 39
10. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stage line 44
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.gateRecords_append line 47
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.recordsBits_append line 55
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.step_roots line 59
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.lowerStage_snapshot line 67
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stage_snapshot line 87
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stages line 98
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stages_snapshot line 104
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.compile_frameForest line 113
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.recordBits_step line 124
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.step_repeat line 132
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.circuitOutput line 139
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.circuitOutput_snapshot line 143
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.finalFrame line 149
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.finalFrame_circuit line 154
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.verifier_stages line 157
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.verifier_output line 176
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_root_mem_lt line 182
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_rootBits_length_le line 187
29. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_records_length_le line 193
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.snapshot_lengths_le line 203
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stage_tokenBits_length_le line 219
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stage_countBits_length_le line 230
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.budgetPolynomial line 238
34. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.tapePolynomial line 242
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.budgetPolynomial_eval line 245
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.tapePolynomial_eval line 253
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.freeFrame_lengths_le line 257
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_gate_count line 273
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_gates_le line 281
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_current_le line 291
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.transition_cost_le_budget line 299
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_lengths_le line 311
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.initial_tokens_length_le line 327
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.transition_tokens_length_le line 340
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.acceptance_tokens_length_le line 359
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.finalFrame_lengths_le line 376
47. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stageEnvelopePolynomial line 392
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stageEnvelopePolynomial_eval line 396
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.timeFrame_stageEnvelope line 402
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.verifier_circuitBits_length_le line 419
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stepExpressions line 442
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.transitionTokens line 450
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.transitionTokens_eq line 455
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.compile_transitionTokens line 474
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ProducerInvariant.stepExpressions_verifier line 508
56. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.Extra line 521
57. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList line 526
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList_getElem?_ctorIdx_eq line 529
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.Extra.enumList_nodup line 533
60. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.(instance at line 535) line 535
61. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.Tape line 539
62. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.Alphabet line 540
63. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.State line 541
64. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.forestPorts line 543
65. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.termTape line 546
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.termPorts line 560
67. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.termPorts_apply line 564
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.termInput line 566
69. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.tapes line 569
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.finishTapes line 584
71. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.tapes_q line 588
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.tapes_raw line 592
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.tapes_capacity line 596
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.termFrame line 600
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.tapes_countdown_tail line 608
76. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.preparedTapes line 623
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.place_emitTapes line 630
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionArena.fill_forest line 638