OAI/Computability/BinPacking/Computation/MachineCloudPadding.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes line 16
2. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.label line 22
3. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.configuration line 26
4. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.statement line 31
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_apply line 46
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.tapes_update line 52
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.stepAux_simulation line 71
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.step_simulation line 98
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Placement.trace line 118
10. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Tape line 135
11. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Tape.enumList line 139
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Tape.enumList_getElem?_ctorIdx_eq line 142
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Tape.enumList_nodup line 146
14. instance OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.(instance at line 148) line 148
15. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Label line 152
16. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.Alphabet line 158
17. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.State line 159
18. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.memory line 161
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.update_count line 174
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.update_scratch line 177
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.update_power line 180
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.update_level line 184
23. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countTape line 188
24. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countView line 196
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countView_left line 205
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countView_right line 207
27. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerTape line 211
28. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerView line 221
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerView_left line 232
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerView_right line 234
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countMemory line 238
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerMemory line 243
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countTapes line 248
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerTapes line 253
35. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.subtractLoop line 260
36. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.program line 268
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.appendTrace line 283
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.countTrace line 287
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.powerTrace line 303
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.subtractStep_zero line 318
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.subtractStep_succ line 328
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.subtractScanTrace line 338
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.subtractTrace line 361
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.branchStep_zero line 381
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.branchStep_succ line 389
46. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.padding line 398
47. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.postTime line 400
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.postTrace line 403
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.initStep line 431
50. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.totalTime line 438
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingTrace line 442
52. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.inputLength line 463
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.count_length_le line 466
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.table_length_le line 473
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.postTime_le line 478
56. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.timePolynomial line 484
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.totalTime_le line 487
58. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.cloudPaddingInTime line 502
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPadding.count_add_padding line 518