proposition: Lemma interp_dom_R1_R2 : forall R1 R2, module R1 R2 -> (forall f, {defined R2 f}+{~defined R2 f}) -> (forall s t, R1 s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall v t, ~ R2 t (Var v)) -> forall (s t : term), Interp_dom R1 R2 s -> one_step (@union _ R1 R2) t s -> Interp_dom R1 R2 t.
proof: Proof. intros R1 R2 module_R1_R2 def_dec R1_reg R2_var s. pattern s; apply term_rec2; clear s. intro n; induction n as [ | n]; intros t Size_t. absurd (1 <= 0); auto with arith. apply Nat.le_trans with (size t); [apply size_ge_one | assumption]. intros s It H; inversion H as [ t1 s1 H' | f lt ls H']; clear H; subst. inversion H' as [d g sigma [H1 | H2]]; clear H'; subst. intros p f k Sub Df. generalize (subterm_in_instantiated_term p d sigma Sub). case_eq (subterm_at_pos d p). intros [x | f' k'] Sub' K. rewrite K. assert (x_in_g := R1_reg _ _ H1 x (var_in_subterm x _ _ Sub' (or_introl _ (eq_refl _)))). destruct (var_in_subterm2 x g) as [q Sub'']. apply in_impl_mem; trivial. rewrite <- K; apply (It q); trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos g q sigma). rewrite Sub''; rewrite K; trivial. injection K; clear K; intros; subst f' k. inversion module_R1_R2 as [M]. apply False_rect; generalize (M _ _ _ Df H1); simpl; rewrite (symb_in_subterm f _ _ Sub'). discriminate. simpl; rewrite eq_symb_bool_refl; apply eq_refl. intros Sub' [x [q [q' [K1 [x_in_d [Sub'' Sub''']]]]]]. assert (x_in_g := R1_reg _ _ H1 x (var_in_subterm x _ _ Sub'' (or_introl _ (eq_refl _)))). destruct (var_in_subterm2 x g) as [q'' Sub4]. apply in_impl_mem; trivial. apply (It (q'' ++ q')); trivial. apply subterm_in_subterm with (apply_subst sigma (Var x)); trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos g q'' sigma). rewrite Sub4; trivial. destruct g as [v | f l]. apply False_rect; apply (R2_var _ _ H2). simpl in It; apply (interp_well_defined_2 R1 R2 _ _ It). apply (Def _ _ _ _ H2). apply at_top; apply (instance (@union _ R1 R2) d (Term f l) sigma); right; trivial. destruct (def_dec f) as [Df | Cf]. apply interp_well_defined_2 with f ls; trivial. right; assumption. assert (Size_ls : forall s, In s ls -> size s <= n). intros s s_in_ls; apply le_S_n; apply Nat.le_trans with (size (Term f ls)); trivial. apply size_direct_subterm; trivial. assert (Hlt : forall t, In t lt -> Interp_dom R1 R2 t). assert (Hls : forall s, In s ls -> Interp_dom R1 R2 s). intros; apply interp_well_defined_1 with f ls; trivial. destruct (one_step_in_list H') as [a [b [l1 [l2 [H'' [H1 H2]]]]]]; subst ls lt. intros t t_in_lt; destruct (in_app_or _ _ _ t_in_lt) as [t_in_l1 | [t_eq_b | t_in_l2]]. apply Hls; apply in_or_app; left; assumption. subst t; apply IHn with a; trivial. apply Size_ls; apply in_or_app; right; left; apply eq_refl. apply interp_well_defined_1 with f (l1 ++ a :: l2); trivial. apply in_or_app; right; left; apply eq_refl. apply Hls; apply in_or_app; do 2 right; assumption. intros [ | i p]; intros g l H Dg; simpl in H. injection H; intros; subst; absurd (defined R2 g); trivial. assert (H'' := nth_error_ok_in i lt). destruct (nth_error lt i) as [ ti | ]. generalize (H'' _ (eq_refl _)); clear H''; intros [l1 [l2 [L1 H'']]]. assert (ti_in_lt : In ti lt). subst; apply in_or_app; right; left; trivial. apply (Hlt _ ti_in_lt p); trivial. discriminate. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec dp)