Interaction of Backtrackings and Strict Constant Mappings on PreTrigger

We merely lift GroundTerm.backtrackFacts_under_constant_mapping_subset_of_composing_with_subs to PreTrigger here.

theorem PreTrigger.affected_rules_eq_of_same_skeleton {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {trg trg2 : PreTrigger sig} (same_skeleton : trg.same_skeleton trg2) : trg.affected_rules_for_backtracking = trg2.affected_rules_for_backtracking

The affected rules for triggers with the PreTrigger.same_skeleton are the same.

theorem PreTrigger.affected_rules_eq_of_composing_with_subs {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {trg : PreTrigger sig} (g : StrictConstantMapping sig) : trg.affected_rules_for_backtracking = { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }.affected_rules_for_backtracking

Since a strict constant mapping does not change term structure, the affected rules of a trigger stay the same when a strict constant mapping is applied after the substitution.

theorem PreTrigger.backtracking_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] (trg : PreTrigger sig) (g : StrictConstantMapping sig) : (∀ (d : sig.C), d ∈ List.flatMap Rule.constants trg.affected_rules_for_backtracking → g d = d) → ∃ (fresh_constant_remapping : StrictConstantMapping sig), (∀ (d : sig.C), ¬d ∈ trg.backtrackFacts.snd → fresh_constant_remapping d = d) ∧ (StrictConstantMapping.toConstantMapping fun (c : sig.C) => if c ∈ trg.backtrackFacts.snd then fresh_constant_remapping c else g c).apply_fact_set trg.backtrackFacts.fst.toSet ⊆ { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }.backtrackFacts.fst.toSet ∧ List.map fresh_constant_remapping trg.backtrackFacts.snd = { rule := trg.rule, subs := g.toConstantMapping.apply_ground_term ∘ trg.subs }.backtrackFacts.snd