OAI/Computability/BinPacking/Packing/PackingGapDefinitions.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.BinPackingGap.PairFirstProjection.Tape line 11
  2. abbrev OAI.BinPackingGap.PairFirstProjection.Tape.enumList line 15
  3. theorem OAI.BinPackingGap.PairFirstProjection.Tape.enumList_getElem?_ctorIdx_eq line 17
  4. theorem OAI.BinPackingGap.PairFirstProjection.Tape.enumList_nodup line 21
  5. instance OAI.BinPackingGap.PairFirstProjection.(instance at line 23) line 23
  6. inductive OAI.BinPackingGap.PairFirstProjection.Label line 27
  7. abbrev OAI.BinPackingGap.PairFirstProjection.Label.enumList line 31
  8. theorem OAI.BinPackingGap.PairFirstProjection.Label.enumList_getElem?_ctorIdx_eq line 33
  9. theorem OAI.BinPackingGap.PairFirstProjection.Label.enumList_nodup line 37
  10. instance OAI.BinPackingGap.PairFirstProjection.(instance at line 39) line 39
  11. abbrev OAI.BinPackingGap.PairFirstProjection.State line 43
  12. def OAI.BinPackingGap.PairFirstProjection.tapes line 45
  13. theorem OAI.BinPackingGap.PairFirstProjection.tapes_input line 51
  14. theorem OAI.BinPackingGap.PairFirstProjection.tapes_counter line 52
  15. theorem OAI.BinPackingGap.PairFirstProjection.tapes_reversed line 53
  16. theorem OAI.BinPackingGap.PairFirstProjection.tapes_output line 54
  17. theorem OAI.BinPackingGap.PairFirstProjection.update_input line 56
  18. theorem OAI.BinPackingGap.PairFirstProjection.update_counter line 61
  19. theorem OAI.BinPackingGap.PairFirstProjection.update_reversed line 66
  20. theorem OAI.BinPackingGap.PairFirstProjection.update_output line 71
  21. def OAI.BinPackingGap.PairFirstProjection.code line 76
  22. def OAI.BinPackingGap.PairFirstProjection.program line 91
  23. abbrev OAI.BinPackingGap.PairFirstProjection.machine line 98
  24. def OAI.BinPackingGap.PairFirstProjection.cfg line 100
  25. theorem OAI.BinPackingGap.PairFirstProjection.scan_true line 104
  26. theorem OAI.BinPackingGap.PairFirstProjection.scan_false line 113
  27. theorem OAI.BinPackingGap.PairFirstProjection.copy_cons line 122
  28. theorem OAI.BinPackingGap.PairFirstProjection.copy_nil line 131
  29. theorem OAI.BinPackingGap.PairFirstProjection.reverse_cons line 140
  30. theorem OAI.BinPackingGap.PairFirstProjection.reverse_nil line 149
  31. theorem OAI.BinPackingGap.PairFirstProjection.scan_trace line 158
  32. theorem OAI.BinPackingGap.PairFirstProjection.copy_trace line 176
  33. theorem OAI.BinPackingGap.PairFirstProjection.reverse_trace line 188
  34. theorem OAI.BinPackingGap.PairFirstProjection.init_eq line 199
  35. theorem OAI.BinPackingGap.PairFirstProjection.projection_trace line 206
  36. def OAI.BinPackingGap.PairFirstProjection.rawTime line 226
  37. def OAI.BinPackingGap.PairFirstProjection.rawRun line 228
  38. def OAI.BinPackingGap.PairFirstProjection.cleanupTapes line 241
  39. theorem OAI.BinPackingGap.PairFirstProjection.cleanup_complete line 243
  40. def OAI.BinPackingGap.PairFirstProjection.computation line 246
  41. theorem OAI.BinPackingGap.PairFirstProjection.finiteAlphabet line 252
  42. theorem OAI.BinPackingGap.inP_to_inNP line 262
  43. theorem OAI.BinPackingGap.classP_subset_classNP line 286
  44. theorem OAI.BinPackingGap.pEqualsNP_iff_np_subset_p line 289
  45. theorem OAI.BinPackingGap.PEqualsNP.inP line 300
  46. structure OAI.BinPackingGap.PromiseProblem line 304
  47. structure OAI.BinPackingGap.PolynomialPromiseReduction line 309
  48. def OAI.BinPackingGap.PromiseNPHard line 317
  49. structure OAI.BinPackingGap.PolynomialPromiseDecider line 322
  50. theorem OAI.BinPackingGap.PolynomialPromiseReduction.inP line 330
  51. theorem OAI.BinPackingGap.PromiseNPHard.pEqualsNP line 349
  52. def OAI.BinPackingGap.packingPromise line 357
  53. def OAI.BinPackingGap.PackingGapReduction.toPromiseReduction line 364
  54. theorem OAI.BinPackingGap.PackingGapNPHard.promiseNPHard line 374