proposition: Lemma interp_dom_interp_dom_1 : forall f l1 l2, ~G f -> acc_sub R (Term f l1) -> refl_trans_clos (one_step_list (one_step R)) l2 l1 -> Interp_dom (Term f l2).
proof: Proof. intros f l1 l2 f_in_H Acc_l1 K1. intros [ | i q] g l Sub g_not_in_H. injection Sub; clear Sub; intros; subst; apply False_rect; apply f_in_H; assumption. simpl in Sub. generalize (nth_error_ok_in i l2); destruct (nth_error 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 rwr_sub_acc_sub_acc_sub with l1 l2; trivial. subst l2; 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)