Renaming Constants apart in a GroundTerm

We lift the PreGroundTerm.rename_constants_apart functionality to GroundTerm.

def GroundTerm.rename_constants_apart {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) : GroundTerm sig

Equations

• term.rename_constants_apart forbidden_constants = ⟨term.val.rename_constants_apart forbidden_constants, ⋯⟩

theorem GroundTerm.rename_constants_apart_constants_fresh {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] [CustomBasicDatastructures.GetFreshInhabitant sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) (c : sig.C) : c ∈ (term.rename_constants_apart forbidden_constants).constants → ¬c ∈ forbidden_constants