OAI/Computability/BinPacking/Reductions/Target.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BinPackingGames.Foundations.Target.Literal line 7
  2. def OAI.BinPackingGames.Foundations.Target.Literal.eval line 12
  3. abbrev OAI.BinPackingGames.Foundations.Target.Clause line 15
  4. def OAI.BinPackingGames.Foundations.Target.Clause.eval line 17
  5. structure OAI.BinPackingGames.Foundations.Target.Formula line 20
  6. def OAI.BinPackingGames.Foundations.Target.Formula.Satisfiable line 24
  7. structure OAI.BinPackingGames.Foundations.Target.PermutationTable line 28
  8. theorem OAI.BinPackingGames.Foundations.Target.PermutationTable.images_injective line 34
  9. theorem OAI.BinPackingGames.Foundations.Target.PermutationTable.images_surjective line 39
  10. structure OAI.BinPackingGames.Foundations.Target.Constraint line 43
  11. def OAI.BinPackingGames.Foundations.Target.Constraint.satisfied line 48
  12. structure OAI.BinPackingGames.Foundations.Target.Instance line 52
  13. def OAI.BinPackingGames.Foundations.Target.countSatisfied line 57
  14. theorem OAI.BinPackingGames.Foundations.Target.countSatisfied_le_length line 63
  15. theorem OAI.BinPackingGames.Foundations.Target.Instance.constraintCount_positive line 72
  16. structure OAI.BinPackingGames.Foundations.Target.RationalError line 78
  17. def OAI.BinPackingGames.Foundations.Target.CompleteAt line 85
  18. def OAI.BinPackingGames.Foundations.Target.SoundAt line 91
  19. structure OAI.BinPackingGames.Foundations.Target.SemanticGapReduction line 96