OAI/Computability/BinPacking/Computation/MachineRegularVertexBlock.lean

GitHub source file

78 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.Tape line 11
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.Alphabet line 12
3. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.State line 13
4. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.Label line 15
5. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.instruction line 20
6. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTapes line 30
7. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps line 34
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.join_trace line 38
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupTraceAt line 42
10. structure OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.Input line 76
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.cleanup_frame line 81
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.suffix_length_le line 95
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_eq line 105
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.cleanupSteps_le line 149
15. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.steps line 163
16. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.timeBound line 167
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.steps_le line 170
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.traceAt line 178
19. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.machine line 197
20. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalClean.machineInTime line 208
21. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.PortLabel line 233
22. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portEntry line 235
23. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portInstruction line 239
24. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portBits line 245
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_eq line 249
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_all line 259
27. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits line 263
28. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps line 268
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.joinTrace line 276
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portPrefixTrace line 280
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portTrace line 309
32. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalTapes line 325
33. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalView line 328
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_left line 333
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalView_right line 336
36. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalStateEquiv line 341
37. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreInstruction line 349
38. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory line 356
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_input line 360
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalMemory_update line 364
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalFrame line 368
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalCoreTrace line 374
43. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTapes line 406
44. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView line 408
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_left line 413
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyView_right line 416
47. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreInstruction line 421
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMemory_update line 427
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyFrame line 432
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyCoreTrace line 438
51. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.Label line 467
52. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalEntry line 474
53. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyEntry line 477
54. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.instruction line 480
55. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.oldCloud line 489
56. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps line 492
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalRowSteps_eq line 496
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_flatMap line 507
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.encodeWords_pair line 513
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.vertexBits_split line 516
61. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps line 529
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalTraceAt line 536
63. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps line 579
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTraceAt line 586
65. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.rowSizeBound line 628
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.rowBits_length_le line 630
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portBits_length_le line 636
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.allRowBits_length_le line 650
69. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portTimeBound line 658
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.portSteps_le line 662
71. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalTimeBound line 694
72. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyTimeBound line 699
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalSteps_le line 703
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummySteps_le line 733
75. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachine line 751
76. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachine line 762
77. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.originalMachineInTime line 773
78. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularVertexBlock.dummyMachineInTime line 793