hasCover_of_nil_edges
plain-language theorem explainer
If a vertex cover instance has an empty edge list then the empty vertex set satisfies the cover predicate and the size bound. Researchers formalizing NP-completeness reductions or exact solvers for vertex cover cite this vacuous base case. The proof is a direct term-mode construction that supplies the empty list and discharges the covering condition by simplification on the empty edge set.
Claim. Let $I$ be a vertex cover instance consisting of a vertex list, an edge list, and bound $k$. If the edge list of $I$ is empty, then there exists a list $S$ of vertices such that the length of $S$ is at most $k$ and every edge of $I$ is incident to a vertex in $S$.
background
The module introduces a vertex cover instance as a structure containing a list of natural-number vertices, a list of edges as pairs of naturals, and a natural-number bound $k$. The predicate Covers $S$ $I$ asserts that every edge in the instance is incident to at least one vertex in $S$. HasCover $I$ is the existential statement that some list $S$ satisfies both the length bound and the Covers predicate.
proof idea
The proof is a term-mode wrapper that refines the witness to the empty list, applies simplification to confirm the length bound, and then uses a contradiction on the empty edge list to discharge the universal quantifier in Covers.
why it matters
The lemma supplies the trivial empty-edge case that closes the definition of HasCover. It supports downstream reasoning about vertex cover within the complexity module, though no direct parent theorems are recorded. The result aligns with the framework's pattern of establishing exact base cases before scaling to larger input sizes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.