Ruleset Triggers

Triggers are still not enough yet. We introduce one more layer on top, which we call RTrigger for Ruleset Trigger. It makes sense that, when we want to chase a set of rules, we only consider triggers that feature rules that indeed occur in the rule set. We capture this simply in a subtype.

def RTrigger {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] (obs : LaxObsoletenessCondition sig) (r : RuleSet sig) : Type (max 0 (max u_3 u_2) u_1)

An RTrigger for a RuleSet $R$ is a Trigger with a rule in $R$.

Equations

• RTrigger obs r = { trg : Trigger obs // trg.rule ∈ r.rules }

def RTrigger.equiv {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : LaxObsoletenessCondition sig} {rs : RuleSet sig} (trg1 trg2 : RTrigger obs rs) : Prop

Two RTriggers are equivalent if the underlying PreTriggers are.

Equations

• trg1.equiv trg2 = trg1.val.equiv trg2.val.toPreTrigger

theorem RTrigger.equiv_of_term_mem_fresh_terms_for_head_disjunct {sig : Signature} [DecidableEq sig.P] [DecidableEq sig.C] [DecidableEq sig.V] {obs : LaxObsoletenessCondition sig} {rs : RuleSet sig} {trg1 trg2 : RTrigger obs rs} {i1 i2 : Nat} {lt1 : i1 < trg1.val.rule.head.length} {lt2 : i2 < trg2.val.rule.head.length} {t : GroundTerm sig} : t ∈ trg1.val.fresh_terms_for_head_disjunct i1 lt1 → t ∈ trg2.val.fresh_terms_for_head_disjunct i2 lt2 → trg1.equiv trg2 ∧ i1 = i2

If a ground term is fresh in two RTriggers for two head indices, then actually these two RTriggers (and indices) need to be equivalent (the same)! Why is this the case? Fresh terms are always Skolem function terms. Therefore they contain a rule id. Since we know that rules are uniquely identified by their id in a RuleSet, we can infer that the rules of the triggers are the same. The head indices are also part of the functional term so a similar argument can be made to show that these need to be equal. To see why the triggers also need to agree on their frontier mapping, we only need to remind ourselves that the Skolem term contains all the mapped frontier terms as arguments.