OAI/Computability/BinPacking/Search/ApproximationImpliesP.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.approximationAccepts line 11
  2. theorem OAI.BinPackingGap.approximationAccepts_none line 15
  3. theorem OAI.BinPackingGap.approximationAccepts_some line 18
  4. theorem OAI.BinPackingGap.approximationAccepts_iff_bins_le line 23
  5. theorem OAI.BinPackingGap.AbsoluteAdditiveAlgorithm.accepts_of_hasPacking line 30
  6. theorem OAI.BinPackingGap.AbsoluteAdditiveAlgorithm.rejects_of_not_hasPacking line 39
  7. theorem OAI.BinPackingGap.PackingGapReduction.approximation_decides line 53
  8. def OAI.BinPackingGap.ApproximationDecisionMachine.borrowPred line 78
  9. def OAI.BinPackingGap.ApproximationDecisionMachine.predWord line 83
  10. theorem OAI.BinPackingGap.ApproximationDecisionMachine.borrowPred_value line 85
  11. theorem OAI.BinPackingGap.ApproximationDecisionMachine.borrowPred_length line 99
  12. theorem OAI.BinPackingGap.ApproximationDecisionMachine.predWord_value line 114
  13. theorem OAI.BinPackingGap.ApproximationDecisionMachine.predWord_length_le line 121
  14. def OAI.BinPackingGap.ApproximationDecisionMachine.nextCount line 126
  15. def OAI.BinPackingGap.ApproximationDecisionMachine.process line 129
  16. theorem OAI.BinPackingGap.ApproximationDecisionMachine.process_length_le line 134
  17. theorem OAI.BinPackingGap.ApproximationDecisionMachine.process_value line 145
  18. theorem OAI.BinPackingGap.ApproximationDecisionMachine.process_test line 161
  19. inductive OAI.BinPackingGap.ApproximationDecisionMachine.Tape line 168
  20. abbrev OAI.BinPackingGap.ApproximationDecisionMachine.Tape.enumList line 172
  21. theorem OAI.BinPackingGap.ApproximationDecisionMachine.Tape.enumList_getElem?_ctorIdx_eq line 174
  22. theorem OAI.BinPackingGap.ApproximationDecisionMachine.Tape.enumList_nodup line 178
  23. instance OAI.BinPackingGap.ApproximationDecisionMachine.(instance at line 180) line 180
  24. inductive OAI.BinPackingGap.ApproximationDecisionMachine.Label line 184
  25. abbrev OAI.BinPackingGap.ApproximationDecisionMachine.Register line 190
  26. abbrev OAI.BinPackingGap.ApproximationDecisionMachine.Alphabet line 191
  27. def OAI.BinPackingGap.ApproximationDecisionMachine.clean line 193
  28. def OAI.BinPackingGap.ApproximationDecisionMachine.read line 194
  29. def OAI.BinPackingGap.ApproximationDecisionMachine.head line 195
  30. def OAI.BinPackingGap.ApproximationDecisionMachine.tapes line 197
  31. theorem OAI.BinPackingGap.ApproximationDecisionMachine.tapes_input line 204
  32. theorem OAI.BinPackingGap.ApproximationDecisionMachine.tapes_binary line 205
  33. theorem OAI.BinPackingGap.ApproximationDecisionMachine.tapes_scratch line 206
  34. theorem OAI.BinPackingGap.ApproximationDecisionMachine.tapes_constant line 207
  35. theorem OAI.BinPackingGap.ApproximationDecisionMachine.tapes_output line 208
  36. theorem OAI.BinPackingGap.ApproximationDecisionMachine.update_input line 210
  37. theorem OAI.BinPackingGap.ApproximationDecisionMachine.update_binary line 213
  38. theorem OAI.BinPackingGap.ApproximationDecisionMachine.update_scratch line 216
  39. theorem OAI.BinPackingGap.ApproximationDecisionMachine.update_constant line 219
  40. theorem OAI.BinPackingGap.ApproximationDecisionMachine.update_output line 222
  41. def OAI.BinPackingGap.ApproximationDecisionMachine.go line 226
  42. def OAI.BinPackingGap.ApproximationDecisionMachine.finish line 229
  43. def OAI.BinPackingGap.ApproximationDecisionMachine.pushConstant line 232
  44. theorem OAI.BinPackingGap.ApproximationDecisionMachine.stepAux_pushConstant line 236
  45. def OAI.BinPackingGap.ApproximationDecisionMachine.orderExit line 249
  46. def OAI.BinPackingGap.ApproximationDecisionMachine.code line 254
  47. def OAI.BinPackingGap.ApproximationDecisionMachine.program line 281
  48. abbrev OAI.BinPackingGap.ApproximationDecisionMachine.machine line 288
  49. theorem OAI.BinPackingGap.ApproximationDecisionMachine.machine_code line 290
  50. theorem OAI.BinPackingGap.ApproximationDecisionMachine.machine_step line 293
  51. def OAI.BinPackingGap.ApproximationDecisionMachine.cfg line 295
  52. theorem OAI.BinPackingGap.ApproximationDecisionMachine.oneStep line 298
  53. theorem OAI.BinPackingGap.ApproximationDecisionMachine.joinTrace line 303
  54. theorem OAI.BinPackingGap.ApproximationDecisionMachine.startSome line 307
  55. theorem OAI.BinPackingGap.ApproximationDecisionMachine.startNone line 313
  56. theorem OAI.BinPackingGap.ApproximationDecisionMachine.readBinTrace line 319
  57. theorem OAI.BinPackingGap.ApproximationDecisionMachine.restoreTrace line 340
  58. def OAI.BinPackingGap.ApproximationDecisionMachine.borrowCost line 354
  59. def OAI.BinPackingGap.ApproximationDecisionMachine.borrowOutput line 359
  60. theorem OAI.BinPackingGap.ApproximationDecisionMachine.borrowCost_le line 364
  61. theorem OAI.BinPackingGap.ApproximationDecisionMachine.drainTrace line 373
  62. theorem OAI.BinPackingGap.ApproximationDecisionMachine.borrowTrace line 392
  63. theorem OAI.BinPackingGap.ApproximationDecisionMachine.decrementTrace line 436
  64. theorem OAI.BinPackingGap.ApproximationDecisionMachine.nameTrace line 443
  65. def OAI.BinPackingGap.ApproximationDecisionMachine.itemsCost line 464
  66. theorem OAI.BinPackingGap.ApproximationDecisionMachine.itemsTrace line 470
  67. theorem OAI.BinPackingGap.ApproximationDecisionMachine.itemsCost_le line 506
  68. theorem OAI.BinPackingGap.ApproximationDecisionMachine.orderExit_eq line 527
  69. theorem OAI.BinPackingGap.ApproximationDecisionMachine.compareTrace line 536
  70. def OAI.BinPackingGap.ApproximationDecisionMachine.someSteps line 557
  71. theorem OAI.BinPackingGap.ApproximationDecisionMachine.someTrace line 562
  72. def OAI.BinPackingGap.ApproximationDecisionMachine.rawTime line 588
  73. theorem OAI.BinPackingGap.ApproximationDecisionMachine.someSteps_le line 591
  74. theorem OAI.BinPackingGap.ApproximationDecisionMachine.init_eq line 616
  75. def OAI.BinPackingGap.ApproximationDecisionMachine.rawRun line 623
  76. def OAI.BinPackingGap.ApproximationDecisionMachine.cleanupTapes line 656
  77. theorem OAI.BinPackingGap.ApproximationDecisionMachine.cleanup_complete line 658
  78. def OAI.BinPackingGap.ApproximationDecisionMachine.computation line 662
  79. theorem OAI.BinPackingGap.ApproximationDecisionMachine.finiteAlphabet line 667
  80. def OAI.BinPackingGap.AbsoluteAdditiveAlgorithm.rawComputation line 681
  81. def OAI.BinPackingGap.PackingGapReduction.approximationComputation line 691
  82. theorem OAI.BinPackingGap.PackingGapReduction.approximationComputation_finiteAlphabet line 704
  83. theorem OAI.BinPackingGap.PackingGapReduction.inP_of_absoluteAdditiveAlgorithm line 723
  84. theorem OAI.BinPackingGap.PackingGapNPHard.pEqualsNP_of_absoluteAdditiveAlgorithm line 730