A trailing nullary constraint has no argument occurrences

These structural identities retain all earlier constraint positions and repeated variables. They make no satisfiability assertion: the interpretation of the nullary relation is separate.

theorem Cslib.Logic.PL.CSP.vars_append_nullary {Rel V : Type} (F : CSP Rel V) (r : Rel) : (F ++ [(r, [])]).vars = F.vars

Appending a nullary scope leaves the variable-occurrence word unchanged.

theorem Cslib.Logic.PL.CSP.occurrences_append_nullary {Rel V : Type} (F : CSP Rel V) (r : Rel) : (F ++ [(r, [])]).occurrences = F.occurrences

A trailing nullary constraint contributes no indexed argument record.

theorem Cslib.Logic.PL.CSP.distinctVars_append_nullary {Rel V : Type} [DecidableEq V] (F : CSP Rel V) (r : Rel) : (F ++ [(r, [])]).distinctVars = F.distinctVars

First-occurrence variable names remain literal when a nullary scope is appended.

theorem Cslib.Logic.PL.CSP.numVars_append_nullary {Rel V : Type} [DecidableEq V] (F : CSP Rel V) (r : Rel) : (F ++ [(r, [])]).numVars = F.numVars

Nullary constraints do not introduce variable names.