OAI/Computability/BinPacking/Computation/MachineCloudPrefix.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.Alphabet line 12
2. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.finish line 14
3. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.loop line 18
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.loopPushBound line 28
5. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes line 32
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_source line 37
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_destination line 43
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.unaryTapes_other line 49
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.update_source line 56
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.update_destination line 69
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_true line 79
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_false line 88
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_succ line 96
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.stepAux_zero line 107
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.step_succ line 119
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.step_zero line 133
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.addTrace line 147
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.addFromTapes line 171
19. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.addInTime line 191
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAddAt.addInTime_steps line 209
21. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.Tape line 229
22. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.Label line 234
23. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.Alphabet line 240
24. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.State line 241
25. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.memory line 243
26. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame line 250
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_query line 253
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_count line 255
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_power line 257
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_level line 259
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_bound line 261
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_remaining line 263
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.frame_total line 265
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.update_frame_query line 268
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.update_frame_count line 276
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.update_frame_power line 284
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.update_frame_level line 292
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.update_frame_remaining line 300
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.update_frame_total line 304
40. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.paddingView line 309
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.paddingView_left line 313
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.paddingView_right line 315
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.placedTapes line 319
44. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.program line 326
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.appendTrace line 342
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.paddingTrace line 346
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.incrementStep line 364
48. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.bodyTime line 373
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.bodyTrace line 378
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.guardStep_succ line 420
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.guardStep_zero line 430
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.zeroTrace line 438
53. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.amount line 452
54. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.cycleTime line 455
55. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.sumFrom line 458
56. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.loopTime line 462
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.loopTrace line 466
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_list line 497
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.sumFrom_eq_offset line 517
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.initStep line 526
61. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.totalTime line 533
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.prefixTrace line 536
63. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.cycleBudget line 564
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.bodyTime_le line 568
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.loopTime_le line 596
66. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.inputLength line 609
67. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.timePolynomial line 612
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.totalTime_le line 619
69. def OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.prefixInTime line 639
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.all_padding_sum line 654
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCloudPrefix.paddingOrder_eq_prefix line 658