CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.head rules graph: generalisation of ADPGraph to S @ (hd_red R) instead of (int_red R #) @ (dp R)
- Leo Ducas, 2007-08-06
Set Implicit Arguments.
Variable Sig : Signature.
Notation term := (term Sig). Notation terms := (vector term).
Notation rule := (rule Sig). Notation rules := (list rule).
Notation lhs := (@lhs Sig). Notation rhs := (@rhs Sig).
Variable S : relation term.
Variable D : rules.
head rules graph
Definition hd_rules_graph a1 a2 := In a1 D /\ In a2 D
/\ exists p, exists s, S (sub s (rhs a1)) (sub s (shift p (lhs a2))).
Lemma restricted_dp_graph : is_restricted hd_rules_graph D.
corresponding chain relation
Definition hd_red_Mod_rule a t u := In a D /\
exists s, S t (sub s (lhs a)) /\ u = sub s (rhs a).
Lemma chain_hd_rules_hd_red_Mod : forall a,
hd_red_Mod_rule a << hd_red_Mod S D.
Lemma hd_red_Mod_chain_hd_rules : forall t u,
hd_red_Mod S D t u -> exists a, hd_red_Mod_rule a t u.
Variable hyp : rules_preserve_vars D.
Lemma hd_red_Mod_rule2_hd_rules_graph : forall a1 a2 t u v,
hd_red_Mod_rule a1 t u -> hd_red_Mod_rule a2 u v -> hd_rules_graph a1 a2.
Lemma hd_red_Mod2_hd_rules_graph : forall t u v,
hd_red_Mod S D t u -> hd_red_Mod S D u v ->
exists a1, exists a2, hd_rules_graph a1 a2.
Lemma hd_rules_graph_incl : forall S D D', incl D D' ->
hd_rules_graph S D << hd_rules_graph S D'.
relation between hd_red_Mod and chain