proposition: Lemma interp_defined : forall t, Interp_dom R1 R2 t -> {s : term | Interp t s}.
proof: Proof. intros t Ht; assert (Acc_t := interp_well_defined R1 R2 t Ht). induction Acc_t as [t Acc_t IH]. destruct t as [x | f l]. exists (Var x); apply Vcase. destruct (def_dec f) as [Df | Cf]. assert (interp_l : forall s, In s (R1_R2_red (Term f l)) -> {u : term | Interp s u}). intros s s_in_red_t; apply IH. apply (Defd R1 R2 f l s Df). rewrite FB12; trivial. apply interp_well_defined_2 with f l; trivial. rewrite FB12; trivial. assert (ll : {ll : list (term * term) | R1_R2_red (Term f l) = (map (fun st => fst st)) ll /\ (forall s s', In (s,s') ll -> Interp s s')}). generalize (R1_R2_red (Term f l)) interp_l. intro k; induction k as [ | s k]. intros _; exists (@nil (term * term)); split; trivial; contradiction. intros interp_sk. destruct (interp_sk s) as [u Isu]. left; trivial. destruct IHk as [kk [Hk Pk]]. intros; apply interp_sk; right; trivial. exists ((s,u) :: kk); split. simpl; rewrite Hk; trivial. simpl; intros t t' [tt'_eq_su | tt'_in_kk]. injection tt'_eq_su; intros; subst; trivial. apply Pk; trivial. destruct ll as [ll [Hl Pl]]. exists (Comb (map (fun st => snd st) ll)). apply Dcase with ll; trivial. assert (interp_l : forall s, In s l -> {u : term | Interp s u}). intros s s_in_l; apply IH. apply (Constr R1 R2 f l s Cf s_in_l). apply interp_well_defined_1 with f l; trivial. assert (ll : {ll : list (term * term) | l = (map (fun st => fst st)) ll /\ (forall s s', In (s,s') ll -> Interp s s')}). generalize l interp_l. intro k; induction k as [ | s k]. intros _; exists (@nil (term * term)); split; trivial; contradiction. intros interp_sk. destruct (interp_sk s) as [u Isu]. left; trivial. destruct IHk as [kk [Hk Pk]]. intros; apply interp_sk; right; trivial. exists ((s,u) :: kk); split. simpl; rewrite Hk; trivial. simpl; intros t t' [tt'_eq_su | tt'_in_kk]. injection tt'_eq_su; intros; subst; trivial. apply Pk; trivial. destruct ll as [ll [Hl Pl]]. exists (Term f (map (fun st => snd st) ll)). apply Ccase with ll; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)