proposition: 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.
proof: Proof. intros. destruct a1 as [l0 r0]. destruct a2 as [l1 r1]. destruct H. simpl in H1. do 2 destruct H1. subst u. rename x into s0. destruct H0. simpl in H2. do 2 destruct H2. subst v. rename x into s1. unfold hd_rules_graph. intuition. simpl. set (p := maxvar l0 + 1). exists p. set (s0' := restrict s0 (vars l0)). set (s1' := restrict (sub_comp s1 (shift_inv_sub p l1)) (vars (shift p l1))). set (s := ASubstitution.union s0' s1'). exists s. assert (compat s0' s1' (vars l0) (vars (shift p l1))). unfold compat. intros. ded (vars_max H3). ded (in_vars_shift_min H4). unfold p in H6. absurd (x <= maxvar l0). lia. hyp. assert (dom_incl s0' (vars l0)). unfold s0'. apply dom_incl_restrict. assert (dom_incl s1' (vars (shift p l1))). unfold s1'. apply dom_incl_restrict. assert (sub s r0 = sub s0' r0). unfold s. eapply sub_union1. apply H5. apply H3. apply hyp. hyp. rewrite H6. assert (sub s0' r0 = sub s0 r0). unfold s0'. sym. apply sub_restrict_incl. apply hyp. hyp. rewrite H7. assert (sub s (shift p l1) = sub s1' (shift p l1)). unfold s. eapply sub_union2. apply H4. apply H3. refl. rewrite H8. assert (sub s1' (shift p l1) = sub s1 l1). unfold s1'. rewrite <- sub_restrict, <- sub_shift. refl. rewrite H9. hyp. Qed.
imports: CoLoR(LogicUtil ATrs RelUtil RelSub SN AShift ADPGraph VecUtil ASubstitution) Coq(List Lia)