mentionsVar
plain-language theorem explainer
The definition returns true exactly when a variable index occurs inside a mixed constraint, which is either a CNF clause or an XOR constraint. Analysts formalizing propagation completeness for hybrid SAT instances cite it when isolating single-variable determining constraints during peeling. Realization is a direct pattern match on the Constraint constructor that delegates to the clause or XOR mention test.
Claim. Let $K$ be a constraint over $n$ variables and let $v$ be a variable index in Fin $n$. Then mentionsVar$(K,v)$ evaluates to true if and only if $v$ appears among the literals of $K$ when $K$ is a clause, or among the listed variables of $K$ when $K$ is an XOR constraint.
background
The Constraint type is defined inductively with two constructors: cnf wrapping a Clause $n$ and xor wrapping an XORConstraint $n$. Variables are abbreviated as Fin $n$. The clause mention predicate scans literals via mentionsVarLit; the XOR predicate tests direct membership in the constraint's vars list. This definition lives inside the PC module whose module comment states that constraints are either CNF-clauses or XOR-checks.
proof idea
One-line wrapper realized by pattern matching on the Constraint inductive: the cnf case applies mentionsVarClause and the xor case applies mentionsVarXOR.
why it matters
The predicate is invoked inside the PC definition, the extractFromPC helper, and the PeelingData and PeelingResult structures. It supplies the variable-occurrence test required to enforce the single-variable coverage condition of propagation completeness. The surrounding module imports UniversalForcingSelfReference, indicating the SAT formalization is intended to support reductions that feed into self-referential forcing arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.