proposition: Lemma interp_defined : forall t, Acc interp_call t -> {t' | Interp t t'}.
proof: Proof. intros t Acc_t; induction Acc_t as [t Acc_t' IH]. assert (Acc_t : Acc interp_call t). apply Acc_intro; apply Acc_t'. clear Acc_t'; destruct t as [x | f l]. exists (Var x); apply Vcase. assert (Il : {ll : list (term * term) | l = map (@fst term term) ll /\ forall t t', In (t,t') ll -> Interp t t'}). assert (IHl : forall t, In t l -> {t' : term | Interp t t'}). intros t t_in_l. apply IH; left; trivial. revert IHl; clear; induction l as [ | t l]; intros IH. exists nil; split; [apply eq_refl | intros; contradiction]. destruct (IHl (tail_set _ IH)) as [ll [H1 H2]]. destruct (IH _ (or_introl _ (eq_refl _))) as [t' H3]. exists ((t,t') :: ll); split; [ subst l; apply eq_refl | intros u u' [uu'_eq_tt' | uu'_in_ll]; [injection uu'_eq_tt'; intros; subst; assumption | apply H2; assumption]]. destruct Il as [ll [H1 H2]]. destruct (Gdec _ _ Rlist_ok _ _ Plist_ok f) as [f_not_in_G | f_in_G]. exists (Term f (map (@snd _ _) ll)). apply notGcase with ll; trivial. rewrite Gdef'; assumption. assert (Ik : {kk : list (term * term) | R_red (Term f l) = map (@fst term term) kk /\ forall t t', In (t,t') kk -> Interp t t'}). assert (IHk : forall t, In t (R_red (Term f l)) -> {t' : term | Interp t t'}). intros t t_in_red; rewrite FB in t_in_red. apply IH; right; trivial. rewrite Gdef'; assumption. revert IHk; generalize ((R_red (Term f l))); clear. intro k; induction k as [ | t k]; intro Hk. exists nil; split; [apply eq_refl | intros; contradiction]. destruct (IHk (tail_set _ Hk)) as [kk [H1 H2]]. destruct (Hk _ (or_introl _ (eq_refl _))) as [t' H3]. exists ((t,t') :: kk); split; [ subst k; apply eq_refl | intros u u' [uu'_eq_tt' | uu'_in_ll]; [injection uu'_eq_tt'; intros; subst; assumption | apply H2; assumption]]. destruct Ik as [kk [K1 K2]]. exists (Comb (Term f (map (@snd _ _) ll) :: (map (@snd _ _) kk))). apply Gcase with ll kk; trivial. rewrite Gdef'; 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)