Interaction of Backtrackings and Strict Constant Mappings on GroundTerm

We merely lift PreGroundTerm.backtrackFacts_under_constant_mapping_subset_of_composing_with_subs to GroundTerm here.

theorem GroundTerm.backtrackFacts_under_constant_mapping_subset_of_composing_with_subs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (term : GroundTerm sig) (term_ruleIds_valid : skolem_ruleIds_valid rl term) (term_disjIdx_valid : skolem_disjIdx_valid rl term term_ruleIds_valid) (term_rule_arity_valid : skolem_rule_arity_valid rl term term_ruleIds_valid) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_term : term.constants ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap Rule.constants rl.rules ⊆ forbidden_constants) : have backtracking := backtrackFacts rl term term_ruleIds_valid term_disjIdx_valid term_rule_arity_valid forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants rl.rules → g d = d) → ∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ backtracking.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) => if c ∈ backtracking.snd then fresh_constant_remapping c else g c).apply_fact_set backtracking.fst.toSet ⊆ (backtrackFacts rl (g.toConstantMapping.apply_ground_term term) ⋯ ⋯ ⋯ (List.map g forbidden_constants)).fst.toSet ∧ List.map fresh_constant_remapping backtracking.snd = (backtrackFacts rl (g.toConstantMapping.apply_ground_term term) ⋯ ⋯ ⋯ (List.map g forbidden_constants)).snd

theorem GroundTerm.backtrackFacts_list_under_constant_mapping_subset_of_composing_with_subs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] [GetFreshInhabitant sig.C] [Inhabited sig.C] (rl : RuleList sig) (terms : List (GroundTerm sig)) (terms_ruleIds_valid : ∀ (t : GroundTerm sig), t ∈ terms → skolem_ruleIds_valid rl t) (terms_disjIdx_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_disjIdx_valid rl t ⋯) (terms_rule_arity_valid : ∀ (t : GroundTerm sig) (mem : t ∈ terms), skolem_rule_arity_valid rl t ⋯) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_terms : List.flatMap constants terms ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap Rule.constants rl.rules ⊆ forbidden_constants) : have backtracking := backtrackFacts_list rl terms terms_ruleIds_valid terms_disjIdx_valid terms_rule_arity_valid forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants rl.rules → g d = d) → ∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ backtracking.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) => if c ∈ backtracking.snd then fresh_constant_remapping c else g c).apply_fact_set backtracking.fst.toSet ⊆ (backtrackFacts_list rl (List.map g.toConstantMapping.apply_ground_term terms) ⋯ ⋯ ⋯ (List.map g forbidden_constants)).fst.toSet ∧ List.map fresh_constant_remapping backtracking.snd = (backtrackFacts_list rl (List.map g.toConstantMapping.apply_ground_term terms) ⋯ ⋯ ⋯ (List.map g forbidden_constants)).snd