OAI/Computability/VertexCover/Reduction/RejectionCount.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.VertexCover.ClauseProjection.Pattern line 41
  2. instance OAI.VertexCover.ClauseProjection.(instance at line 43) line 43
  3. theorem OAI.VertexCover.ClauseProjection.pattern_card line 45
  4. def OAI.VertexCover.ClauseProjection.patternEquiv line 47
  5. def OAI.VertexCover.ClauseProjection.flipSign line 50
  6. theorem OAI.VertexCover.ClauseProjection.flipSign_flipSign line 52
  7. def OAI.VertexCover.ClauseProjection.literalAt line 55
  8. def OAI.VertexCover.ClauseProjection.game line 58
  9. def OAI.VertexCover.ClauseProjection.clauseValue line 73
  10. theorem OAI.VertexCover.ClauseProjection.clause_eval_iff line 77
  11. def OAI.VertexCover.ClauseProjection.honestLabeling line 92
  12. theorem OAI.VertexCover.ClauseProjection.honest_satisfies line 99
  13. theorem OAI.VertexCover.ClauseProjection.perfect_complete line 109
  14. def OAI.VertexCover.ClauseProjection.assignmentOf line 114
  15. theorem OAI.VertexCover.ClauseProjection.satisfies_iff line 117
  16. def OAI.VertexCover.ClauseProjection.unsatisfiedClauses line 136
  17. theorem OAI.VertexCover.ClauseProjection.reject_of_unsatisfied line 140
  18. theorem OAI.VertexCover.ClauseProjection.rejection_count line 153