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] [CustomBasicDatastructures.GetFreshInhabitant sig.C] [Inhabited sig.C] (term : GroundTerm sig) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_term : term.constants ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap Rule.constants term.rules ⊆ forbidden_constants) : have backtracking := term.backtrackFacts forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants term.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 (CustomBasicDatastructures.List.toSet backtracking.fst) ⊆ CustomBasicDatastructures.List.toSet ((g.toConstantMapping.apply_ground_term term).backtrackFacts (List.map g forbidden_constants)).fst ∧ List.map fresh_constant_remapping backtracking.snd = ((g.toConstantMapping.apply_ground_term term).backtrackFacts (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] [CustomBasicDatastructures.GetFreshInhabitant sig.C] [Inhabited sig.C] (terms : List (GroundTerm sig)) (forbidden_constants : List sig.C) (forbidden_constants_subsumes_terms : List.flatMap constants terms ⊆ forbidden_constants) (forbidden_constants_subsumes_rules : List.flatMap Rule.constants (List.flatMap rules terms) ⊆ forbidden_constants) : have backtracking := backtrackFacts_list terms forbidden_constants; ∀ (g : StrictConstantMapping sig), (∀ (d : sig.C), d ∈ List.flatMap Rule.constants (List.flatMap rules terms) → 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 (CustomBasicDatastructures.List.toSet backtracking.fst) ⊆ CustomBasicDatastructures.List.toSet (backtrackFacts_list (List.map g.toConstantMapping.apply_ground_term terms) (List.map g forbidden_constants)).fst ∧ List.map fresh_constant_remapping backtracking.snd = (backtrackFacts_list (List.map g.toConstantMapping.apply_ground_term terms) (List.map g forbidden_constants)).snd