InCover_cons
plain-language theorem explainer
This lemma asserts that any vertex x belongs to the covering set formed by prepending x to an arbitrary list xs. It supplies a basic membership fact for inductive constructions in vertex cover arguments within complexity analysis. The proof is a one-line simplification that directly invokes the membership definition of InCover.
Claim. For any natural number $x$ and list $xs$ of natural numbers, $x$ belongs to the list $x :: xs$, i.e., the set $x :: xs$ covers the vertex $x$.
background
The Complexity.VertexCover module treats complexity pairs as functions of input size. Its central predicate InCover is defined by membership: a list S covers vertex v precisely when v lies in S. This supplies the elementary fact needed to build covering sets inductively by list cons.
proof idea
The proof is a one-line wrapper that applies the simp tactic to the definition of InCover, reducing the membership claim for the cons constructor to a trivial list fact.
why it matters
The lemma supplies a foundational membership step inside the vertex-cover development of the Recognition Science complexity module. It supports later arguments that construct explicit covers and aligns with the need for precise set-membership facts when deriving discrete structures from the T0-T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.