proposition: Lemma interp_dom_interp_dom_2 : forall mark, (forall v u, P u v -> mrel mark (dp R) u v) -> forall s t, acc_sub R s -> acc_sub R t -> rdp_step (axiom P) R t s -> Interp_dom s -> Interp_dom t.
proof: Proof. intros mark P_in_dpR s t Acc_sub_s Acc_sub_t K Is. inversion K as [_f ls l H1 H2]; clear K; subst. inversion H as [_t _fl sigma K1 K2 K3]; clear H; subst. assert (_K := P_in_dpR _ _ K1). inversion _K as [t fk K]; clear _K; subst. destruct fk as [x | f k]. inversion K; subst; apply False_rect; apply (R_var _ _ H). injection K3; clear K3; intros; subst. inversion K as [u v p f2 l2 H Sub Df2]; subst. assert (f2_in_H : ~G (mark f2)). apply (head_P_in_H mark P_in_dpR _ _ nil (mark f2) l2 K1). rewrite empty_subst_is_id; apply eq_refl. intros [ | i q] g k' Sub' g_not_in_H. simpl in Sub'; injection Sub'; clear Sub'; intros; subst; apply False_rect; apply f2_in_H; assumption. simpl in Sub'. generalize (nth_error_ok_in i (map (apply_subst sigma) l2)); destruct (nth_error (map (apply_subst sigma) l2) i) as [ai | ]; [idtac | discriminate]. intro K'; destruct (K' _ (eq_refl _)) as [l2' [l2'' [L K'']]]; clear K'. apply acc_subterms_3 with q ai; trivial. apply Acc_sub_t; simpl; rewrite K''; apply in_or_app; right; left; apply eq_refl. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec dp graph_dp terminaison interp)