OAI/Computability/VertexCover/Reduction/ReductionSound.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.ClauseProjection.baseGap line 43
  2. theorem OAI.VertexCover.ClauseProjection.baseGap_pos line 45
  3. theorem OAI.VertexCover.ClauseProjection.baseGap_le_third line 48
  4. def OAI.VertexCover.ClauseProjection.repetitionAlphabetBudget line 52
  5. theorem OAI.VertexCover.ClauseProjection.repetitionAlphabetBudget_pos line 54
  6. def OAI.VertexCover.ClauseProjection.repetitionBase line 57
  7. theorem OAI.VertexCover.ClauseProjection.repetitionBase_mem line 59
  8. theorem OAI.VertexCover.ClauseProjection.exists_repetition_length line 71
  9. def OAI.VertexCover.ClauseProjection.repetitionLength line 82
  10. def OAI.VertexCover.ClauseProjection.reduction line 85
  11. theorem OAI.VertexCover.ClauseProjection.reduction_alphabets line 88
  12. theorem OAI.VertexCover.ClauseProjection.reduction_complete line 92
  13. theorem OAI.VertexCover.ClauseProjection.reduction_sound line 98