OAI/Computability/BinPacking/Computation/MachineCeilingPower.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Tape line 12
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList line 16
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList_getElem?_ctorIdx_eq line 19
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Tape.enumList_nodup line 23
5. instance OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.(instance at line 25) line 25
6. inductive OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Label line 29
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Label.enumList line 34
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Label.enumList_getElem?_ctorIdx_eq line 37
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Label.enumList_nodup line 41
10. instance OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.(instance at line 43) line 43
11. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.Alphabet line 47
12. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.State line 48
13. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.memory line 50
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.update_work line 60
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.update_power line 63
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.update_saved line 66
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.update_level line 69
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.update_fuel line 72
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.update_product line 75
20. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.compareLoop line 81
21. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.scaleLoop line 91
22. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.program line 100
23. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.overflow line 123
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.compareStep_zero line 125
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_zero line 135
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.compareStep_succ_succ line 145
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.compareTrace line 155
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.replicate_encodeWord line 180
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.compareRestoredTrace line 184
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.appendTrace line 205
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.scaleStep_succ line 209
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.scaleStep_zero line 220
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.scaleScanTrace line 230
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.scaleTrace line 248
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.cleanupTrace line 270
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.guardStep_succ line 281
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.guardStep_zero line 292
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.decideStep line 303
39. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.prefixTime line 315
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.prefixTrace line 317
41. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.coreTime line 344
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.coreTrace line 349
43. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.roundBudget line 377
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le line 379
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.prefixTime_le_roundBudget line 384
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.continuingTime_le line 390
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.coreTime_le line 398
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.initStep line 423
49. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.totalTime line 431
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.searchTrace line 433
51. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.timeBound line 453
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.totalTime_le line 455
53. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.timePolynomial line 462
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.timePolynomial_encoding line 465
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.paddingTrace line 469
56. def OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.paddingInTime line 477
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCeilingPower.paddingOutput_bounds line 488