OAI/Computability/VertexCover/PCP/Target.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.UniqueGames.Foundations.Target.Literal line 9
  2. def OAI.UniqueGames.Foundations.Target.Literal.eval line 14
  3. abbrev OAI.UniqueGames.Foundations.Target.Clause line 17
  4. def OAI.UniqueGames.Foundations.Target.Clause.eval line 19
  5. structure OAI.UniqueGames.Foundations.Target.Formula line 22
  6. def OAI.UniqueGames.Foundations.Target.Formula.Satisfiable line 26
  7. structure OAI.UniqueGames.Foundations.Target.PermutationTable line 30
  8. theorem OAI.UniqueGames.Foundations.Target.PermutationTable.images_injective line 36
  9. theorem OAI.UniqueGames.Foundations.Target.PermutationTable.images_surjective line 41
  10. structure OAI.UniqueGames.Foundations.Target.Constraint line 45
  11. def OAI.UniqueGames.Foundations.Target.Constraint.satisfied line 50
  12. structure OAI.UniqueGames.Foundations.Target.Instance line 54
  13. def OAI.UniqueGames.Foundations.Target.countSatisfied line 59
  14. theorem OAI.UniqueGames.Foundations.Target.countSatisfied_le_length line 65
  15. theorem OAI.UniqueGames.Foundations.Target.Instance.constraintCount_positive line 74
  16. structure OAI.UniqueGames.Foundations.Target.RationalError line 80
  17. def OAI.UniqueGames.Foundations.Target.CompleteAt line 87
  18. def OAI.UniqueGames.Foundations.Target.SoundAt line 93
  19. structure OAI.UniqueGames.Foundations.Target.SemanticGapReduction line 98