OAI/Computability/VertexCover/Main.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.Machine.MainReduction.gapInput line 49
  2. def OAI.VertexCover.Machine.MainReduction.gapInputPoly line 52
  3. def OAI.VertexCover.Machine.MainReduction.base line 54
  4. def OAI.VertexCover.Machine.MainReduction.basePoly line 56
  5. theorem OAI.VertexCover.Machine.MainReduction.base_toLC line 59
  6. def OAI.VertexCover.Machine.MainReduction.repeated line 62
  7. def OAI.VertexCover.Machine.MainReduction.repeatedPoly line 65
  8. def OAI.VertexCover.Machine.MainReduction.repetitionIso line 68
  9. theorem OAI.VertexCover.Machine.MainReduction.repeated_complete line 71
  10. theorem OAI.VertexCover.Machine.MainReduction.repeated_sound line 77
  11. def OAI.VertexCover.Machine.MainReduction.construct line 82
  12. def OAI.VertexCover.Machine.MainReduction.constructPoly line 85
  13. theorem OAI.VertexCover.Machine.MainReduction.construct_complete line 89
  14. theorem OAI.VertexCover.Machine.MainReduction.construct_sound line 96
  15. def OAI.VertexCover.Machine.MainReduction.reduction line 103
  16. theorem OAI.VertexCover.explicit_cover_gap line 113

    Distinct definitions of this name: ComparatorChallenges/VertexCover.lean:145 (same statement text; different proof or body). Qualify references as OAI.VertexCover.explicit_cover_gap@path.

  17. theorem OAI.VertexCover.every_fixed_factor_below_two line 115

    Distinct definitions of this name: ComparatorChallenges/VertexCover.lean:148 (same statement text; different proof or body). Qualify references as OAI.VertexCover.every_fixed_factor_below_two@path.