Variables of concatenated formulas

The variables of a concatenation of formulas (Cslib.Logic.PL.CNF.vars) are those of the first formula followed by those of the second. Reductions that assemble a formula from blocks of clauses use this to count or locate the variables of each block.

Main results

• Cslib.Logic.PL.CNF.vars_append: the variables of φ ++ ψ.

theorem Cslib.Logic.PL.CNF.vars_append {V : Type u_1} (φ ψ : CNF V) : (φ ++ ψ).vars = φ.vars ++ ψ.vars

The variables of a concatenation of formulas are those of the first formula, then those of the second.