proposition: Lemma interp_well_defined : forall t, Interp_dom t -> Acc interp_call t.
proof: Proof. intro t; pattern t; apply term_rec3; clear t. intros v _. apply Acc_intro; intros t K; inversion K. intros f l IH K. apply Acc_intro; intros t K'; inversion K'; subst. apply IH; trivial. destruct (in_split _ _ H1) as [l1 [l2 K'']]. apply interp_dom_subterm with (Term f l) (length l1 :: nil); trivial. subst l; simpl; rewrite nth_error_at_pos; apply eq_refl. apply Acc_inv with (Term f l); trivial. generalize (K nil f l (eq_refl _) H2). set (s := Term f l) in *; clearbody s; clear. intro Acc_s; rewrite acc_with_subterm in Acc_s. induction Acc_s as [s Acc_s' IH]. assert (Acc_s : Acc (union term (one_step R) direct_subterm) s). apply Acc_intro; apply Acc_s'. clear Acc_s'. apply Acc_intro; intros t K; inversion K; clear K; subst. apply IH; right; assumption. apply IH; left; assumption. 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)