The Backtracking Triggers in the Chase indeed is already part of the Chase

The goal of this file is to show backtracking_of_loaded_trigger_in_node. This states that the backtracking of a trigger that is loaded for a chase node indeed already occurs in that chase node (as intuition suggests). However, since fresh constants are introduced when backtracking, this only holds true under the application of a ConstantMapping. Showing the existence of an appropriate mapping is also part of the theorem. Furthermore, we require this mapping to map each constant in the mapped body of the trigger and each constant in the rule set to itself. Intuitively, the mapping shall only remap the constants that where freshly introduced.

theorem ChaseBranch.backtracking_of_loaded_trigger_in_node {sig : Signature} [DecidableEq sig.C] [DecidableEq sig.V] [DecidableEq sig.P] {obs : ObsolescenceCondition sig} {kb : KnowledgeBase sig} [GetFreshInhabitant sig.C] [Inhabited sig.C] {cb : ChaseBranch obs kb} {node : ChaseNode obs kb.rules} (node_mem : node ∈ cb.toChaseDerivation) (rl : RuleList sig) (rl_rs_eq : ∀ (r : Rule sig), r ∈ rl.rules ↔ r ∈ kb.rules.rules) (trg : PreTrigger sig) (trg_loaded : trg.loaded node.facts) : ∃ (g : ConstantMapping sig), g.apply_fact_set (PreTrigger.backtrackFacts rl trg ⋯ ⋯ ⋯).fst.toSet ⊆ node.facts ∧ ∀ (d : sig.C), d ∈ (List.flatMap Fact.constants trg.mapped_body).toSet ∪ kb.rules.constants → g d = GroundTerm.const d