CLRS-Lean
Chapter 34. NP-Completeness
34.5. NP-Complete Problems
34.5. HAM-CYCLE
34.5. The typed VERTEX-COVER to HAM-CYCLE reduction

Imports

import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Reduction.Construction
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Reduction.EncodingBounds
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Reduction.Completeness
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.HamiltonianCycle.Reduction.Soundness

The typed VERTEX-COVER to HAM-CYCLE reduction

This facade exports the total well-formed construction, its bidirectional typed semantic correctness theorem, and its cubic encoded-size bound.

              namespace CLRS.Chapter34.HamiltonianCycleReductiontheorem vertexCoverToHamiltonianInstance_correct
    {I : VertexCoverInstance} (hwellFormed : I.WellFormed) :
    I.HasVertexCover ↔
      (vertexCoverToHamiltonianInstance I).HasHamiltonianCycle :=
  ⟨vertexCoverToHamiltonianInstance_complete hwellFormed,
    vertexCoverToHamiltonianInstance_sound hwellFormed⟩end CLRS.Chapter34.HamiltonianCycleReduction