OAI/Computability/BinPacking/Computation/MachineLazyTableRuntime.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.Tape line 13
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.Tape.enumList line 18
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.Tape.enumList_getElem?_ctorIdx_eq line 22
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.Tape.enumList_nodup line 26
5. instance OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.(instance at line 28) line 28
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.State line 32
7. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.clean line 34
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.clean_pair line 37
9. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.splitRoles line 40
10. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.splitView line 41
11. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.dummyRoles line 45
12. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.dummyView line 46
13. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.oldRoles line 50
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.splitRoles_left line 54
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.splitRoles_right line 57
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.dummyRoles_left line 60
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.dummyRoles_right line 63
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.oldRoles_injective line 66
19. inductive OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.Label line 68
20. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.program line 78
21. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.frame line 115
22. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.initialTapes line 120
23. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.loopTapes line 122
24. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.finalTapes line 127
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.joinTrace line 129
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.dummyTrace line 133
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.oldTrace line 162
28. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.prefixSteps line 194
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.prefixTrace line 197
30. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.vertexBlock line 279
31. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.bodySteps line 283
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.frame_old_empty line 289
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.bodyTrace line 294
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.drainPhase line 406
35. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.finishSteps line 417
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.finishTrace line 419
37. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.remaining line 474
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.remaining_zero line 476
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.remaining_done line 477
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.remaining_cons line 479
41. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.inputBlocks line 485
42. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.outputBlocks line 488
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.vertexBlock_codec line 491
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.encodeWords_flatMap line 497
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.inputBlocks_codec line 503
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.outputBlocks_codec line 510
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.input_table_codec line 516
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.output_table_codec line 527
49. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.loopSteps line 539
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.loopTrace line 547
51. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.totalSteps line 588
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.tableTrace line 592
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.dummyRows_length_le line 607
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.bodySteps_le line 618
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.output_length_le line 739
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.loopSteps_le line 756
57. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.timePolynomial line 788
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.timePolynomial_eval line 791
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.totalSteps_le line 795
60. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.machine line 826
61. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.machine_alphabet_finite line 837
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.initial_configuration line 843
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.finalTapes_input line 850
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.finalTapes_output line 851
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.finalTapes_work_empty line 853
66. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTable.machineInTime line 857
67. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.rawProgram line 876
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.sourceMachine_eq line 884
69. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.cleanupTapes line 888
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.cleanup_complete line 892
71. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.terminalRun line 896
72. def OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime line 906
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyTableRuntime.finite_alphabet line 913