OAI/Computability/VertexCover/Reduction/Soundness.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.ClauseProjection.falseFormula line 44
  2. theorem OAI.VertexCover.ClauseProjection.falseFormula_unsat line 47
  3. def OAI.VertexCover.ClauseProjection.inputFormula line 53
  4. def OAI.VertexCover.ClauseProjection.InputSAT line 56
  5. theorem OAI.VertexCover.ClauseProjection.inputFormula_sat line 59
  6. def OAI.VertexCover.ClauseProjection.binaryReduction line 65
  7. theorem OAI.VertexCover.ClauseProjection.binaryReduction_complete line 68
  8. theorem OAI.VertexCover.ClauseProjection.binaryReduction_sound line 74
  9. def OAI.VertexCover.rawGraph line 86
  10. theorem OAI.VertexCover.rawGraph_completeness line 90
  11. theorem OAI.VertexCover.rawLabelCover_soundness line 99