Compaction preserves the listed CNF incidence graph

Main results

• Cslib.Complexity.SAT.incidenceGraph_compact: the entire listed graph is unchanged, including variable indices, clause indices, repeated edge occurrences and their order.

References

This is an elementary consequence of the existing first-occurrence numbering conventions.

theorem Cslib.Complexity.SAT.incidenceGraph_compact {V : Type} [DecidableEq V] (φ : Logic.PL.CNF V) : incidenceGraph φ.compact = incidenceGraph φ

Compaction changes literal labels without changing any vertex or edge of the listed graph.