proposition: Lemma interp_well_defined : forall R1 R2 t, Interp_dom R1 R2 t -> Acc (interp_call R1 R2) t.
proof: Proof. intros R1 R2 t; pattern t; apply term_rec3; clear t. intros v H; apply Acc_intro; intros s Call_s_t; inversion Call_s_t. intros f l IHl H; apply Acc_intro. intros s Call_s_t; inversion Call_s_t as [f1 l' s' not_def_f s_in_l | f2 l' s' def_f s_R_fl]; subst. apply IHl; trivial. apply interp_well_defined_1 with f l; trivial. apply Acc_inv with (Term f l); trivial. assert (Acc_fl := H nil f l (eq_refl _) def_f). revert Acc_fl; generalize (Term f l); clear. intros t Acc_t; rewrite acc_with_subterm in Acc_t. induction Acc_t as [t Acc_t' IH]. apply Acc_intro. intros s Call_s_t; inversion Call_s_t as [f1 l s' not_def_f2 s_in_l | f2 l s' def_f2 s_R_fl]; subst. apply IH; right; trivial. apply IH; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)