OAI/Computability/BinPacking/CookLevin/ValidityMachine.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.Alphabet line 13
2. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.Ports line 15
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.frame line 23
4. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.frame_remaining line 28
5. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.frame_reversed line 33
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.frame_count line 38
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.frame_other line 43
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.frame_self line 49
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.update_remaining line 53
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.update_reversed line 63
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.update_count line 73
12. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.seed line 79
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.loop line 85
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.seedPushBound line 97
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.loopPushBound line 101
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.seedStep line 105
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.loopStep_zero line 113
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.loopStep_succ line 122
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.tokenBits_append line 132
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.tokenBits_or line 136
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.tokenBits_false line 138
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.tokenBits_closeOr line 140
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.tokenBits_replicate_succ line 145
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.replicate_push line 152
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.loopTrace line 160
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.closureTrace line 187
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.closureInTime line 208
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.increment_count line 227
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.machine line 235
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OrClosure.machineTrace line 247
31. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Alphabet line 268
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.chain line 270
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.inputMap line 276
34. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.Label line 278
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.statement line 282
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.frame line 289
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.frame_current line 292
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.frame_remaining line 295
39. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.counter_frame line 298
40. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.emitted_frame line 306
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.increment_frame line 320
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.tokens line 325
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.tokens_zero line 328
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.tokens_succ line 330
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.steps line 339
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.trace line 343
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.SelectorLoop.steps_le line 389
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.loopMap line 405
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.closurePorts line 407
50. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.Label line 415
51. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.copyStatement line 423
52. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.statement line 430
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.steps line 445
54. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.Ready line 449
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.emitted_update line 456
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.frame_updates line 472
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.tokens_nonempty line 476
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.closed_frame line 480
59. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.trace line 491
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.steps_le line 627
61. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.inTime line 633
62. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.machine line 649
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ValidityMachine.Nonempty.machineTrace line 661