OAI/Computability/BinPacking/Computation/PoweringMachineRow.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.Runtime.statementPushBound line 8
2. def OAI.BinPackingGames.Foundations.Complexity.Runtime.maxLabelPushes line 18
3. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.maxLabelPushes_ge line 23
4. def OAI.BinPackingGames.Foundations.Complexity.Runtime.programPushBound line 35
5. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.statement_le_programPushBound line 38
6. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.stepAuxStackLength line 43
7. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.iterateSizeBound line 86
8. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.executionSizeBound line 98
9. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.stepStackLength line 121
10. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.initialStackLength line 134
11. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.haltedOutputLength line 141
12. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.outputLength_le line 145
13. theorem OAI.BinPackingGames.Foundations.Complexity.Runtime.encodedOutputLength line 157
14. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.Buffer line 173
15. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.emptyBuffer line 175
16. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.readSlots line 181
17. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.fill line 190
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.fill_apply line 193
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.fill_all line 204
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readSlots line 211
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_readAll line 227
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_readSlots line 241
23. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.writeSlots line 249
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_writeSlots line 254
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_writeSlots line 269
26. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.blockStmt line 285
27. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.finishAt line 292
28. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.blockMapAt line 297
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockStmt line 301
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.statementPushBound_blockMapAt line 308
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockStmt line 316
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.stepAux_blockMapAt line 330
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.step_blockMapAt line 341
34. def OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.machine line 358
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineFixedBlockMap.machine_statementPushBound line 369
36. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.Field line 381
37. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.inputSize line 383
38. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.fieldEquiv line 385
39. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.inputEquiv line 389
40. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.packData line 392
41. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.packData_inputEquiv line 395
42. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.basePredicate line 400
43. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.leftMatches line 404
44. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.rightMatches line 408
45. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.firstMatch line 412
46. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.firstMatch_spec line 415
47. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.firstMatch_none line 422
48. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.edgeAccept line 426
49. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.edgeAccept_of_matches line 432
50. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.rowAccept line 440
51. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.rowAccept_eq_true line 444
52. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.rowBlock line 450
53. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.rowBlock_at line 456
54. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodeBit line 463
55. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodeBits line 465
56. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodeBits_append line 469
57. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodeBits_graphWords line 475
58. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodeBits_length_le line 482
59. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.readEncodedSlots line 494
60. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedSlots line 507
61. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.stepAux_readEncodedAll line 526
62. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_readEncodedSlots line 542
63. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.writeEncodedSlots line 550
64. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.stepAux_writeEncodedSlots line 558
65. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_writeEncodedSlots line 575
66. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodedBlockStmt line 592
67. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.encodedBlockAt line 599
68. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.statementPushBound_encodedBlockAt line 603
69. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockStmt line 612
70. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.stepAux_encodedBlockAt line 627
71. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.step_encodedBlockAt line 638
72. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.rowAt line 655
73. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.machine line 660
74. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.machine_statementPushBound line 671
75. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRow.machineInTime line 676