OAI/Computability/BinPacking/Model.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.encodeWord line 9

   Also declared: ComparatorChallenges/BinPackingGap.lean:9 (same declaration text).

2. def OAI.BinPackingGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet line 17

   Also declared: ComparatorChallenges/BinPackingGap.lean:17 (same declaration text).

3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.pairBits line 23

   Also declared: ComparatorChallenges/BinPackingGap.lean:23 (same declaration text).

4. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier line 26

   Also declared: ComparatorChallenges/BinPackingGap.lean:26 (same declaration text).

5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.NPVerifier.Accepts line 32

   Also declared: ComparatorChallenges/BinPackingGap.lean:32 (same declaration text).

6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.InNP line 37

   Also declared: ComparatorChallenges/BinPackingGap.lean:37 (same declaration text).

7. def OAI.BinPackingCompleteness.BinaryEncoding.bitsValue line 44

   Also declared: ComparatorChallenges/BinPackingGap.lean:44 (same declaration text).

8. def OAI.BinPackingCompleteness.BinaryEncoding.frame line 48

   Also declared: ComparatorChallenges/BinPackingGap.lean:48 (same declaration text).

9. def OAI.BinPackingCompleteness.BinaryEncoding.parseFrame line 52

   Also declared: ComparatorChallenges/BinPackingGap.lean:52 (same declaration text).

10. def OAI.BinPackingCompleteness.BinaryEncoding.nameBits line 59

    Also declared: ComparatorChallenges/BinPackingGap.lean:59 (same declaration text).

11. def OAI.BinPackingCompleteness.BinaryEncoding.parseName line 61

    Also declared: ComparatorChallenges/BinPackingGap.lean:61 (same declaration text).

12. structure OAI.BinPackingGap.Instance line 72

    Also declared: ComparatorChallenges/BinPackingGap.lean:72 (same declaration text).

13. abbrev OAI.BinPackingGap.Instance.Item line 80

    Also declared: ComparatorChallenges/BinPackingGap.lean:80 (same declaration text).

14. structure OAI.BinPackingGap.Packing line 84

    Also declared: ComparatorChallenges/BinPackingGap.lean:84 (same declaration text).

15. def OAI.BinPackingGap.HasPacking line 88

    Also declared: ComparatorChallenges/BinPackingGap.lean:88 (same declaration text).

16. def OAI.BinPackingGap.singletonPacking line 90

    Also declared: ComparatorChallenges/BinPackingGap.lean:90 (same declaration text).

17. theorem OAI.BinPackingGap.exists_packing line 103

    Also declared: ComparatorChallenges/BinPackingGap.lean:103 (same declaration text).

18. def OAI.BinPackingGap.opt line 106

    Also declared: ComparatorChallenges/BinPackingGap.lean:106 (same declaration text).

19. def OAI.BinPackingGap.IndividualConfiguration line 110

    Also declared: ComparatorChallenges/BinPackingGap.lean:110 (same declaration text).

20. instance OAI.BinPackingGap.(instance at line 113) line 113
21. def OAI.BinPackingGap.NumericalSize line 116

    Also declared: ComparatorChallenges/BinPackingGap.lean:116 (same declaration text).

22. instance OAI.BinPackingGap.(instance at line 118) line 118
23. theorem OAI.BinPackingGap.NumericalSize.positive line 125

    Also declared: ComparatorChallenges/BinPackingGap.lean:125 (same declaration text).

24. def OAI.BinPackingGap.NumericalSize.multiplicity line 130

    Also declared: ComparatorChallenges/BinPackingGap.lean:130 (same declaration text).

25. def OAI.BinPackingGap.NumericalSize.capacityBound line 133

    Also declared: ComparatorChallenges/BinPackingGap.lean:133 (same declaration text).

26. theorem OAI.BinPackingGap.NumericalSize.capacityBound_spec line 136

    Also declared: ComparatorChallenges/BinPackingGap.lean:136 (same declaration text).

27. def OAI.BinPackingGap.TypeConfiguration line 141

    Also declared: ComparatorChallenges/BinPackingGap.lean:141 (same declaration text).

28. theorem OAI.BinPackingGap.TypeConfiguration.count_lt_bound line 148

    Also declared: ComparatorChallenges/BinPackingGap.lean:148 (same declaration text).

29. def OAI.BinPackingGap.TypeConfiguration.boundedCounts line 159

    Also declared: ComparatorChallenges/BinPackingGap.lean:159 (same declaration text).

30. theorem OAI.BinPackingGap.TypeConfiguration.boundedCounts_injective line 162

    Also declared: ComparatorChallenges/BinPackingGap.lean:162 (same declaration text).

31. instance OAI.BinPackingGap.TypeConfiguration.(instance at line 170) line 170
32. instance OAI.BinPackingGap.TypeConfiguration.(instance at line 174) line 174
33. def OAI.BinPackingGap.FractionalCover.Feasible line 183

    Also declared: ComparatorChallenges/BinPackingGap.lean:183 (same declaration text).

34. def OAI.BinPackingGap.FractionalCover.objective line 186

    Also declared: ComparatorChallenges/BinPackingGap.lean:186 (same declaration text).

35. def OAI.BinPackingGap.FractionalCover.objectiveSet line 188

    Also declared: ComparatorChallenges/BinPackingGap.lean:188 (same declaration text).

36. def OAI.BinPackingGap.FractionalCover.value line 191

    Also declared: ComparatorChallenges/BinPackingGap.lean:191 (same declaration text).

37. def OAI.BinPackingGap.individualMatrix line 196

    Also declared: ComparatorChallenges/BinPackingGap.lean:196 (same declaration text).

38. def OAI.BinPackingGap.individualLP line 199

    Also declared: ComparatorChallenges/BinPackingGap.lean:199 (same declaration text).

39. def OAI.BinPackingGap.typeMatrix line 202

    Also declared: ComparatorChallenges/BinPackingGap.lean:202 (same declaration text).

40. def OAI.BinPackingGap.typeLP line 205

    Also declared: ComparatorChallenges/BinPackingGap.lean:205 (same declaration text).

41. abbrev OAI.BinPackingGap.RawInstance line 208

    Also declared: ComparatorChallenges/BinPackingGap.lean:208 (same declaration text).

42. abbrev OAI.BinPackingGap.RawReductionOutput line 210

    Also declared: ComparatorChallenges/BinPackingGap.lean:210 (same declaration text).

43. def OAI.BinPackingGap.RawInstance.Valid line 214

    Also declared: ComparatorChallenges/BinPackingGap.lean:214 (same declaration text).

44. def OAI.BinPackingGap.RawInstance.ratValue line 217

    Also declared: ComparatorChallenges/BinPackingGap.lean:217 (same declaration text).

45. theorem OAI.BinPackingGap.RawInstance.den_pos line 219

    Also declared: ComparatorChallenges/BinPackingGap.lean:219 (same declaration text).

46. def OAI.BinPackingGap.RawInstance.toInstance line 222

    Also declared: ComparatorChallenges/BinPackingGap.lean:222 (same declaration text).

47. structure OAI.BinPackingGap.RawPacking line 232

    Also declared: ComparatorChallenges/BinPackingGap.lean:232 (same declaration text).

48. def OAI.BinPackingGap.RawPacking.load line 238

    Also declared: ComparatorChallenges/BinPackingGap.lean:238 (same declaration text).

49. def OAI.BinPackingGap.RawPacking.Feasible line 242

    Also declared: ComparatorChallenges/BinPackingGap.lean:242 (same declaration text).

50. abbrev OAI.BinPackingGap.BinaryEncoding.natBits line 251

    Also declared: ComparatorChallenges/BinPackingGap.lean:251 (same declaration text).

51. abbrev OAI.BinPackingGap.BinaryEncoding.parseNat line 253

    Also declared: ComparatorChallenges/BinPackingGap.lean:253 (same declaration text).

52. def OAI.BinPackingGap.BinaryEncoding.listBits line 255

    Also declared: ComparatorChallenges/BinPackingGap.lean:255 (same declaration text).

53. def OAI.BinPackingGap.BinaryEncoding.pairBits line 259

    Also declared: ComparatorChallenges/BinPackingGap.lean:259 (same declaration text).

54. def OAI.BinPackingGap.BinaryEncoding.optionBits line 262

    Also declared: ComparatorChallenges/BinPackingGap.lean:262 (same declaration text).

55. abbrev OAI.BinPackingGap.BinaryEncoding.Parser line 266

    Also declared: ComparatorChallenges/BinPackingGap.lean:266 (same declaration text).

56. def OAI.BinPackingGap.BinaryEncoding.parsePair line 268

    Also declared: ComparatorChallenges/BinPackingGap.lean:268 (same declaration text).

57. def OAI.BinPackingGap.BinaryEncoding.parseListAux line 274

    Also declared: ComparatorChallenges/BinPackingGap.lean:274 (same declaration text).

58. def OAI.BinPackingGap.BinaryEncoding.parseList line 283

    Also declared: ComparatorChallenges/BinPackingGap.lean:283 (same declaration text).

59. def OAI.BinPackingGap.BinaryEncoding.decode line 286

    Also declared: ComparatorChallenges/BinPackingGap.lean:286 (same declaration text).

60. def OAI.BinPackingGap.BinaryEncoding.rawInstanceBits line 290

    Also declared: ComparatorChallenges/BinPackingGap.lean:290 (same declaration text).

61. def OAI.BinPackingGap.BinaryEncoding.assignmentBits line 293

    Also declared: ComparatorChallenges/BinPackingGap.lean:293 (same declaration text).

62. def OAI.BinPackingGap.BinaryEncoding.rawPackingBits line 295

    Also declared: ComparatorChallenges/BinPackingGap.lean:295 (same declaration text).

63. def OAI.BinPackingGap.BinaryEncoding.packingResultBits line 298

    Also declared: ComparatorChallenges/BinPackingGap.lean:298 (same declaration text).

64. def OAI.BinPackingGap.BinaryEncoding.rawReductionOutputBits line 300

    Also declared: ComparatorChallenges/BinPackingGap.lean:300 (same declaration text).

65. def OAI.BinPackingGap.BinaryEncoding.parseRawInstance line 303

    Also declared: ComparatorChallenges/BinPackingGap.lean:303 (same declaration text).

66. def OAI.BinPackingGap.BinaryEncoding.decodeRawInstance line 305

    Also declared: ComparatorChallenges/BinPackingGap.lean:305 (same declaration text).

67. abbrev OAI.BinPackingGap.BitLanguage line 311

    Also declared: ComparatorChallenges/BinPackingGap.lean:313 (same declaration text).

68. def OAI.BinPackingGap.InP line 313

    Also declared: ComparatorChallenges/BinPackingGap.lean:315 (same declaration text).

69. def OAI.BinPackingGap.ClassP line 320

    Also declared: ComparatorChallenges/BinPackingGap.lean:322 (same declaration text).

70. def OAI.BinPackingGap.ClassNP line 322

    Also declared: ComparatorChallenges/BinPackingGap.lean:324 (same declaration text).

71. def OAI.BinPackingGap.PEqualsNP line 324

    Also declared: ComparatorChallenges/BinPackingGap.lean:326 (same declaration text).

72. structure OAI.BinPackingGap.AbsoluteAdditiveAlgorithm line 326

    Also declared: ComparatorChallenges/BinPackingGap.lean:328 (same declaration text).

73. structure OAI.BinPackingGap.PackingGapReduction line 335

    Also declared: ComparatorChallenges/BinPackingGap.lean:337 (same declaration text).

74. def OAI.BinPackingGap.PackingGapNPHard line 349

    Also declared: ComparatorChallenges/BinPackingGap.lean:351 (same declaration text).