OAI/Computability/BinPacking/PCP/Initialization.lean

GitHub source file

69 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.Alphabet line 15
2. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.Ports line 17
3. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.Label line 19
4. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList line 24
5. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList_getElem?_ctorIdx_eq line 27
6. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.Label.enumList_nodup line 31
7. instance OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.(instance at line 33) line 33
8. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.statement line 37
9. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.resultTapes line 56
10. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.resultTapes_other line 65
11. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.setupInTime line 71
12. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.tableSetupInTime line 161
13. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.program line 188
14. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Setup.machine line 191
15. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.Context line 210
16. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.RowCommand line 211
17. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits line 213
18. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.vector_list_ofFn line 218
19. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.bitValues_ofFn line 223
20. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.relationBits_values line 232
21. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands line 240
22. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.rowContext line 249
23. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.rowValues line 253
24. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.encodedRow line 259
25. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_bits line 265
26. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands line 296
27. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockWords line 301
28. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.tableWords_eq_blocks line 308
29. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands line 319
30. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_bits line 325
31. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.headerCommands_length line 339
32. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.headerInTime line 343
33. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.encodeWords_flatMap line 368
34. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_bits line 374
35. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.rowCommands_length_le line 381
36. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.flatMap_length_le line 389
37. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommands_length_le line 400
38. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTime line 411
39. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn line 440
40. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockCommandsIn_bits line 444
41. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.EmitRows.blockInTimeAmbient line 453
42. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.headerPlan line 492
43. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.rowPlan line 493
44. inductive OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.Label line 495
45. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.headerEntry line 507
46. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.rowEntry line 510
47. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.clearNext line 513
48. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.program line 516
49. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.machine line 550
50. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.program_setup line 563
51. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.program_guard line 567
52. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.program_headLookup line 570
53. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.program_compare line 574
54. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Driver.program_increment line 577
55. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.inputTapes line 589
56. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.rowsBits line 593
57. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.headerBits line 596
58. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.setupTapes line 600
59. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.loopTapes line 608
60. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.loopStart line 617
61. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.setupResult_eq line 621
62. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.headerResult_eq line 627
63. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.machineInitial_eq line 632
64. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.setupInTime line 642
65. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.headerView_at line 661
66. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.headerInTime line 671
67. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.time line 709
68. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.time_eq line 711
69. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Initialization.initializeInTime line 715