OAI/Computability/BinPacking/CookLevin/CellsTokensAlignment.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Alphabet line 16
2. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.chain line 18
3. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.SymbolSpec line 22
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.payloadTokens line 29
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.symbolTokens line 32
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.inputMap line 40
7. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.Label line 42
8. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.statement line 50
9. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.addressSteps line 71
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.addressTrace line 73
11. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.steps line 108
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.trace line 111
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Payload.steps_le line 172
14. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.Label line 180
15. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.firstLabels line 189
16. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.secondLabels line 190
17. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.statement line 192
18. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.steps line 208
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.trace line 213
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Symbol.steps_le line 273
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tableAt line 287
22. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokensFrom line 290
23. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokens line 293
24. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokensFrom_succ line 295
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.tokens_eq_ofFn line 305
26. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.Label line 313
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.symbolLabels line 318
28. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.statement line 321
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.stepsFrom line 328
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.steps line 332
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.traceFrom line 334
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.trace line 370
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.stepsFrom_le line 380
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.steps_le line 390
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.inTime line 393
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.machine line 410
37. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.Row.machineInTime line 422
38. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.Ports line 444
39. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.Alphabet line 445
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.rowMap line 447
41. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.rowPorts line 453
42. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame line 455
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_index line 459
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_remaining line 462
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_capacity line 465
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.ext_ports line 468
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.update_remaining line 477
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.update_index line 485
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.update_capacity line 493
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_emitted line 497
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.frame_ready line 506
52. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.Label line 533
53. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.rowLabels line 538
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.statement line 542
55. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.Agrees line 550
56. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.guardStep_zero line 554
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.guardStep_succ line 563
58. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.nextStep line 573
59. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.tokens line 590
60. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.steps line 594
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.trace line 598
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.steps_le line 641
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadRowsLoop.tokens_eq_forTokens line 651
64. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.symbolSpec line 671
65. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.symbolTable line 679
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.payloadRowTokens line 683
67. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.symbolTokens_eq_initialCellTokens line 686
68. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PayloadCellsMachine.payloadRowTokens_eq line 705
69. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsTokensAlignment.cellsInterval_append line 728
70. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsTokensAlignment.cellsInterval_full line 737
71. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsTokensAlignment.prefix_eq_interval line 741
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsTokensAlignment.payload_eq_interval line 748
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CellsTokensAlignment.cells_eq_streams line 760