Chase Derivation

Now we go from a ChaseDerivationSkeleton to a ChaseDerivation.

The chase starts on an initial fact set and then applies triggers until all triggers are obsolete, which might only be the case after infinitely many steps. This whole process needs to be "fair", i.e. a trigger that is Trigger.active needs to be not active after finitely many steps. This can happen by applying the trigger itself or another trigger that will make the former obsolete.

We should note that chase derivations usually start on a Database, i.e. a finite fact set where all terms are constants. This is what we demand for a ChaseBranch later but for now it is more convenient for us to relax this condition since it is not relevant for most basic definitions and results. What we gain by relaxing the condition is that we can drop an abitrary number of ChaseNodes from the beginning of a derivation and still be left with a derivation. This gives the ChaseDerivation a more coinductive behavior that conveniently alignes with the PossiblyInfiniteList that is used to provide the basic structure of the derivation skeleton.

The goal of the chase is to eventually build a most general (i.e. universal) model of a given KnowledgeBase by iteratively satisfying all triggers and thereby all rules. For the more generic ChaseDerivation, we cannot quite expect this as a result but we can already show that the ChaseDerivationSkeleton.result models all of the rules in ChaseDerivation.result_models_rules.

The ChaseDerivation Structure

The backbone of the ChaseDerivation is a ChaseDerivationSkeleton with additional conditions.

1. Each trigger used in the derivation must be active for the previous fact set.
2. The derivation needs to be fair. That is, for each trigger, there exists a step in the derivation from which on the trigger is not active.

Expressing the conditions in terms of the machinery available form the PossiblyInfiniteList is admittedly quite convoluted. As part of the framework built around the ChaseDerivation, we will also restate these conditions in a more accessible way. See e.g. ChaseDerivation.fairness'.

structure ChaseDerivation {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : ObsolescenceCondition sig) (rules : RuleSet sig) extends ChaseDerivationSkeleton obs rules : Type (max (max u_1 u_2) u_3)

• branch : PossiblyInfiniteList (ChaseNode obs rules)
• isSome_head : self.branch.head.isSome = true
• triggers_exist (n : Nat) (before : ChaseNode obs rules) : before ∈ (self.branch.drop n).head → let after := (self.branch.drop n).tail.head; exists_trigger_opt_fs obs rules before after
• triggers_active (n : Nat) (before : ChaseNode obs rules) : before ∈ (self.branch.drop n).head → ∀ (after : ChaseNode obs rules), after ∈ (self.branch.drop n).tail.head → ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ after.origin ∧ orig.fst.val.active before.facts
• fairness (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (i : Nat), (∃ (node : ChaseNode obs rules), node ∈ (self.branch.drop i).head ∧ ¬trg.val.active node.facts) ∧ ∀ (j : Nat) (node2 : ChaseNode obs rules), node2 ∈ (self.branch.drop i).tail.get? j → ¬trg.val.active node2.facts

Basic Definitions

Here we introduce some auxiliary definitions and theorems and we lift some of the machinery of the underlying PossiblyInfiniteList to ChaseDerivation. Some have already been lifted to ChaseDerivationSkeleton.

@[implicit_reducible]

instance ChaseDerivation.instMembershipChaseNode {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} : Membership (ChaseNode obs rules) (ChaseDerivation obs rules)

Membership of ChaseNodes in the ChaseDerivation directly corresponds to membership in the ChaseDerivationSkeleton.

Equations

• ChaseDerivation.instMembershipChaseNode = { mem := fun (cd : ChaseDerivation obs rules) (node : ChaseNode obs rules) => node ∈ cd.toChaseDerivationSkeleton }

theorem ChaseDerivation.mem_def {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {e : ChaseNode obs rules} : e ∈ cd ↔ e ∈ cd.toChaseDerivationSkeleton

Unfolds the Membership definition.

theorem ChaseDerivation.mem_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {e : ChaseNode obs rules} : e ∈ cd ↔ ∃ (n : Nat), cd.branch.get? n = some e

An element is a member of the derivation iff it occurs at some index in the underlying branch.

def ChaseDerivation.derivation_for_skeleton {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (l2 : ChaseDerivationSkeleton obs rules) (suffix : l2 <:+ cd.toChaseDerivationSkeleton) : ChaseDerivation obs rules

Each suffix of the underlying ChaseDerivationSkeleton is itself a ChaseDerivation.

Equations

• cd.derivation_for_skeleton l2 suffix = { toChaseDerivationSkeleton := l2, triggers_active := ⋯, fairness := ⋯ }

The "next" ChaseNode

Compared to the ChaseDerivationSkeleton we can show some additional results for next.

theorem ChaseDerivation.active_trigger_origin_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next : ChaseNode obs rules} (eq : cd.next = some next) : (next.origin.get ⋯).fst.val.active cd.head.facts

The trigger used to derive ChaseDerivationSkeleton.next is active for ChaseDerivationSkeleton.head.

theorem ChaseDerivation.isSome_next_iff_trg_ex {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} : cd.next.isSome = true ↔ ∃ (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules), trg.val.active cd.head.facts

The ChaseDerivationSkeleton.next node is not none if and only if some trigger is active on ChaseDerivationSkeleton.head.

ChaseDerivation Suffixes

Suffixes on ChaseDerivations allow us to state the fairness condition more nicely.

def ChaseDerivation.IsSuffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd1 cd2 : ChaseDerivation obs rules) : Prop

Equations

• (cd1 <:+ cd2) = (cd1.toChaseDerivationSkeleton <:+ cd2.toChaseDerivationSkeleton)

def ChaseDerivation.«term_<:+_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

theorem ChaseDerivation.mem_of_mem_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation obs rules} (suffix : cd1 <:+ cd2) (node : ChaseNode obs rules) : node ∈ cd1 → node ∈ cd2

Members of our suffix are also our members.

theorem ChaseDerivation.subderivation_of_node_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {node : ChaseNode obs rules} (node_mem : node ∈ cd) : ∃ (cd2 : ChaseDerivation obs rules), cd2.head = node ∧ cd2 <:+ cd

Each ChaseNode in the ChaseDerivation induces a subderivation.

theorem ChaseDerivation.fairness' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (cd2 : ChaseDerivation obs rules), cd2 <:+ cd ∧ ∀ (node : ChaseNode obs rules), node ∈ cd2 → ¬trg.val.active node.facts

Fairness can be stated as: For each trigger, there exists a subderivation such that the trigger is not active for all nodes in the subderivation.

Tail

def ChaseDerivation.tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) (next_some : cd.next.isSome = true) : ChaseDerivation obs rules

Equations

• cd.tail next_some = cd.derivation_for_skeleton (cd.tail next_some) ⋯

theorem ChaseDerivation.head_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next_some : cd.next.isSome = true} : some (cd.tail next_some).head = cd.next

The ChaseDerivationSkeleton.head of the tail is ChaseDerivationSkeleton.next.

@[simp]

theorem ChaseDerivation.head_tail' {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next_some : cd.next.isSome = true} : (cd.tail next_some).head = cd.next.get next_some

The ChaseDerivationSkeleton.head of the tail is ChaseDerivationSkeleton.next.

theorem ChaseDerivation.next_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next_some : cd.next.isSome = true} (next : ChaseNode obs rules) : next ∈ cd.next → next ∈ cd.tail next_some

ChaseDerivationSkeleton.next is a member of the tail.

theorem ChaseDerivation.mem_iff_eq_head_or_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {node : ChaseNode obs rules} : node ∈ cd ↔ node = cd.head ∨ ∃ (h : cd.next.isSome = true), node ∈ cd.tail h

A node is a member if and only if it is either the head or it is a member of the tail.

theorem ChaseDerivation.suffix_iff_eq_or_suffix_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation obs rules} : cd1 <:+ cd2 ↔ cd1 = cd2 ∨ ∃ (h : cd2.next.isSome = true), cd1 <:+ cd2.tail h

A derivation is a suffix of another if and only if both are the same or the first is a suffix of the second's tail.

Induction Principle for Members

We lift ChaseDerivationSkeleton.mem_rec to ChaseDerivation.

@[reducible, inline]

abbrev ChaseDerivation.Node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} (cd : ChaseDerivation obs rules) : Type (max 0 (max u_3 u_2) u_1)

Equations

• cd.Node = { node : ChaseNode obs rules // node ∈ cd }

def ChaseDerivation.Node.cast_suffix {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd cd2 : ChaseDerivation obs rules} (suffix : cd <:+ cd2) (node : cd.Node) : cd2.Node

A Node of our suffix can be cast into our Node type.

Equations

• ChaseDerivation.Node.cast_suffix suffix node = ⟨node.val, ⋯⟩

theorem ChaseDerivation.mem_rec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {motive : cd.Node → Prop} (head : motive ⟨cd.head, ⋯⟩) (step : ∀ (cd2 : ChaseDerivation obs rules) (suffix : cd2 <:+ cd), motive ⟨cd2.head, ⋯⟩ → ∀ (next : ChaseNode obs rules) (next_mem : next ∈ cd2.next), motive ⟨next, ⋯⟩) (node : cd.Node) : motive node

If we want to show a motive for all nodes in a derivation, it is enough to show the motive for the head and for the next node in each abitrary subderivation where the motive already holds for the head. This can be used with the induction tactic.

theorem ChaseDerivation.mem_tail_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next_some : cd.next.isSome = true} {node : ChaseNode obs rules} : node ∈ cd.tail next_some ↔ ∃ (cd2 : ChaseDerivation obs rules), cd2 <:+ cd ∧ cd2.next = some node

A node is a member of the tail if and only if there is a subderivation where the node is in the ChaseDerivationSkeleton.next position.

Subset Monotonicity of Facts in ChaseNodes

Compared to ChaseDerivationSkeleton, we get a couple of nice implications out of the subset monotonicity of fact sets. For example, we can never see the same ChaseNode twice as otherwise the trigger in second occurrence would already be obsolete.

theorem ChaseDerivation.facts_node_subset_every_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : ChaseNode obs rules) : node ∈ cd → cd.head.facts ⊆ node.facts

Each member's facts contain the head facts. Note that this extends to arbitrary pairs of members since each member always induces a subderivation where it acts as the head.

theorem ChaseDerivation.mem_suffix_of_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation obs rules} (suffix : cd1 <:+ cd2) (node : ChaseNode obs rules) : node ∈ cd2 → node.facts ⊆ cd1.head.facts ∨ node ∈ cd1

A first implication of facts_node_subset_every_mem is that, considering one of our subderivations, each of our members either has all of its facts contained in the head of the subderivation or it is itself a member of the subderivation.

theorem ChaseDerivation.head_not_mem_tail {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (h : cd.next.isSome = true) : ¬cd.head ∈ cd.tail h

The head cannot occur in the tail. Otherwise, it would be introduced using a trigger but then this trigger is already obsolete since all the facts from head already occur in the very beginning. We use ObsolescenceCondition.contains_trg_result_implies_cond here.

theorem ChaseDerivation.eq_of_suffix_of_head_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd1 cd2 : ChaseDerivation obs rules} (suffix : cd1 <:+ cd2) (head_mem : cd2.head ∈ cd1) : cd1 = cd2

By head_not_mem_tail, if we have a suffix but our head occurs in the suffix, then our suffix is equal to us.

theorem ChaseDerivation.suffix_of_suffix_of_suffix_of_head_mem {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd cd1 cd2 : ChaseDerivation obs rules} : cd1 <:+ cd → cd2 <:+ cd → cd2.head ∈ cd1 → cd2 <:+ cd1

And now by eq_of_suffix_of_head_mem, if we have two suffixes $C$ and $D$, and the head of $D$ occurs in $C$, then $D$ is a suffix of $C$. This may seem obvious even without the above results but it is really not even though it aligns well with one's intuition. Imagine that a ChaseNode could occur multiple times in a ChaseDerivation. Then we may have a case where $C$ is a subderivation of $D$, $D$ is not a subderivation of $C$ but $D$ occurs in $C$.

Predecessor Relation

Since we learned that ChaseNodes cannot occur multiple times in the same ChaseDerivation, the predecessor relation defined on ChaseDerivationSkeleton is now a total order on ChaseDerivation.Node. This is particularly nice, since we can do this while completely ignoring indices of the nodes in the underlying PossiblyInfiniteList.

theorem ChaseDerivation.predecessor_iff {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (n1 n2 : cd.Node) : n1 ≼ n2 ↔ ∃ (cd2 : ChaseDerivation obs rules), cd2 <:+ cd ∧ cd2.head = n1.val ∧ n2.val ∈ cd2

We could also define the predecessor relation directly on ChaseDerivations. This theorem shows how this would look.

theorem ChaseDerivation.predecessor_antisymm {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 : cd.Node} : n1 ≼ n2 → n2 ≼ n1 → n1 = n2

The predecessor relation is antisymmetric.

theorem ChaseDerivation.predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 n3 : cd.Node} : n1 ≼ n2 → n2 ≼ n3 → n1 ≼ n3

The predecessor relation is transitive.

theorem ChaseDerivation.fairness_prec {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) : ∃ (node : cd.Node), ∀ (node2 : cd.Node), node ≼ node2 → ¬trg.val.active node2.val.facts

We can express fairness in terms of the predecessor relation: For each trigger, there is a node such that the trigger is not active for each of the node's successors.

The strict version of the predecessor is a strict total order on ChaseDerivation.Node for the ChaseDerivation.

theorem ChaseDerivation.strict_predecessor_asymmetric {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 : cd.Node} : n1 ≺ n2 → ¬n2 ≺ n1

The strict predecessor relation is asymmetric.

theorem ChaseDerivation.strict_predecessor_trans {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 n3 : cd.Node} : n1 ≺ n2 → n2 ≺ n3 → n1 ≺ n3

The strict predecessor relation is transitive.

theorem ChaseDerivation.head_strict_prec_next {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {next : ChaseNode obs rules} (mem : next ∈ cd.next) : ⟨cd.head, ⋯⟩ ≺ ⟨next, ⋯⟩

The ChaseDerivationSkeleton.head is a strict predecessor of ChaseDerivationSkeleton.next.

theorem ChaseDerivation.facts_not_subset_of_strict_predecessor {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {n1 n2 : cd.Node} : n1 ≺ n2 → ¬n2.val.facts ⊆ n1.val.facts

The facts of a strict successor cannot be a subset of our facts. This is because strict successor nodes can only be introduced by active triggers. But if a trigger only produces facts that already exist, then it cannot be active.

Chase Result

Opposed to the ChaseDerivationSkeleton, the result is now a model for all rules.

theorem ChaseDerivation.result_models_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} : cd.result.modelsRules rules

The result is a model of all rules. This is true because otherwise, there would be an active trigger on the result. But then, this trigger needs to be active for some node and the hence it needs to become inactive at some point due to fairness. Hence it cannot be active on the result. Contradiction!

Terms in the Chase

We make some general observations about certain terms that might occur in the chase.

1. Constants can only originate directly from rules or from the initial fact set. No other constants can be introduced.
2. Functional terms can either also originate from the initial fact set or they are introduced as fresh terms by a trigger.

The second observation entails that the precense of a functional term that does not occur in the initial fact set implies that the trigger that introduces this term must have been applied in some ChaseNode.

theorem ChaseDerivation.constants_node_subset_constants_fs_union_constants_rules {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} {node : ChaseNode obs rules} (node_mem : node ∈ cd) : node.facts.constants ⊆ cd.head.facts.constants ∪ rules.head_constants

Constants in the chase can only come from the initial fact set or from a constant in a rule.

theorem ChaseDerivation.functional_term_originates_from_some_trigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : cd.Node) {t : GroundTerm sig} (t_is_func : ∃ (func : SkolemFS sig), ∃ (ts : List (GroundTerm sig)), ∃ (arity_ok : ts.length = func.arity), t = GroundTerm.func func ts arity_ok) (t_mem : t ∈ node.val.facts.terms) : t ∈ cd.head.facts.terms ∨ ∃ (node2 : cd.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node2.val.origin ∧ t ∈ orig.fst.val.fresh_terms_for_head_disjunct ↑orig.snd ⋯

Each functional term in the chase originates as a fresh term from a trigger if it was not already part of the initial fact set.

theorem ChaseDerivation.trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : cd.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ cd.head.facts.terms ∨ ∃ (node2 : cd.Node), node2 ≼ node ∧ ∃ (orig : (trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules) × Fin trg.val.mapped_head.length), orig ∈ node2.val.origin ∧ orig.fst.equiv trg ∧ ↑orig.snd = disj_idx

If a functional term occurs in the chase, then the trigger that introduces this term must have been used in the chase, unless the term already occurs in the initial fact set.

theorem ChaseDerivation.result_of_trigger_introducing_functional_term_occurs_in_chase {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (node : cd.Node) {t : GroundTerm sig} (t_mem_node : t ∈ node.val.facts.terms) {trg : RTrigger { cond := obs.cond, monotone := ⋯ } rules} {disj_idx : Nat} {lt : disj_idx < trg.val.rule.head.length} (t_mem_trg : t ∈ trg.val.fresh_terms_for_head_disjunct disj_idx lt) : t ∈ cd.head.facts.terms ∨ trg.val.mapped_head[disj_idx].toSet ⊆ node.val.facts

If a functional term occurs in the chase, then the result of the trigger that introduces this term is contained in the current node, unless the functional term already occurs in the initial fact set.

Minimal Nodes with given Properties

If a property hold for a given node in the chase, then there must be a "first" node for which this property holds. That means that this node is minimal with respect to the ≺ relation. The result itself is prop_for_node_has_minimal_such_node and is shown via prop_for_nat_has_minimal_such_nat. This forces us to take into account specific node indices and therefore requires auxiliary theorems, mainly get?_branch_injective, which is shown using node_has_unique_position.

theorem ChaseDerivation.prop_for_node_has_minimal_such_node {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : ObsolescenceCondition sig} {rules : RuleSet sig} {cd : ChaseDerivation obs rules} (prop : cd.Node → Prop) (n : cd.Node) : prop n → ∃ (n2 : cd.Node), prop n2 ∧ ∀ (n3 : cd.Node), n3 ≺ n2 → ¬prop n3