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.C] [DecidableEq sig.V] [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.C] [DecidableEq sig.V] [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

theorem GroundTerm.rename_constants_apart_preserves_ruleId_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) (rl : RuleList sig) : skolem_ruleIds_valid rl term → skolem_ruleIds_valid rl (term.rename_constants_apart forbidden_constants)

theorem GroundTerm.rename_constants_apart_preserves_disjIdx_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) (rl : RuleList sig) (h : skolem_ruleIds_valid rl term) : skolem_disjIdx_valid rl term h → skolem_disjIdx_valid rl (term.rename_constants_apart forbidden_constants) ⋯

theorem GroundTerm.rename_constants_apart_preserves_rule_arity_validity {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) (rl : RuleList sig) (h : skolem_ruleIds_valid rl term) : skolem_rule_arity_valid rl term h → skolem_rule_arity_valid rl (term.rename_constants_apart forbidden_constants) ⋯