proposition: Lemma cdp_criterion_local : forall R, (forall x t, ~ (R t (Var x))) -> (forall s t, R s t -> forall x, In x (var_list s) -> In x (var_list t)) -> (forall f, {constructor R f} + {defined R f}) -> forall t, Acc (cdp_step R) t -> (forall s, active_direct_subterm s t -> Acc (C_step R) s) -> Acc (C_step R) t.
proof: Proof. intros R HR RR CD. intros t Acc_t; induction Acc_t as [t Acc_t IH]. intros Acc_l; destruct t as [x | f l]. apply Context_Acc_var; assumption. simpl active_direct_subterm in Acc_l. assert (Acc_l' := Acc_C_step_acc_c_in_context _ _ _ Acc_l). rewrite acc_filtering in Acc_l'. clear Acc_l; rename Acc_l' into Acc_l. set (actives_l := actives f 0 l). generalize (eq_refl actives_l). unfold actives_l at 2. clearbody actives_l. intro H; rewrite <- H in Acc_l. revert l H IH Acc_t. induction Acc_l as [actives_l Acc_l IHl]; intros l AH IH Acc_t. assert (Acc_l' : Acc (one_step_list (C_step R)) actives_l). apply Acc_intro; assumption. clear Acc_l; rename Acc_l' into Acc_l. rewrite <- acc_one_step_list in Acc_l. apply Acc_intro; intros s H; destruct s as [x1 | f1 l1]. apply Context_Acc_var; assumption. inversion H as [t1 t2 H' | f' n l1' l2 H']; clear H; subst. inversion H' as [t1 t2 sigma t1_R_t2 H1 H2]; clear H'. destruct t2 as [x | g k]. absurd (R t1 (Var x)); trivial; apply HR. simpl in H2; injection H2; clear H2; intros; subst g l. assert (H'' : forall n t, size t <= n -> active_subterm t (apply_subst sigma t1) -> Acc (C_step R) t). intro n; induction n as [ | n]. intros t St; absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t); trivial; apply size_ge_one. intros [x | g h] St A. apply Context_Acc_var; trivial. assert (Acc_h : forall t, In t h -> active_subterm t (apply_subst sigma t1) -> Acc (C_step R) t). intros t t_in_h At; apply IHn; trivial. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); apply size_direct_subterm; simpl; trivial. destruct (CD g) as [Cg | Dg]. simpl; apply context_acc_subterms; trivial. intros t t_in_h; apply Acc_h. revert t_in_h; clear; unfold active_in_list, shifted_active_in_list; generalize 0. induction h as [ | s h]. simpl; intros n [[ | i] [_ H]]; discriminate. intros n [[ | i] [H1 H2]]; simpl in H2. injection H2; clear H2; intros; left; assumption. right; apply IHh with (S n). exists i; split; trivial. revert H1; rewrite Nat.add_comm; simpl; rewrite Nat.add_comm; trivial. apply refl_trans_clos_is_trans with (Term g h); trivial. right; left; trivial. rewrite active_is_active in A. destruct A as [p [Ap Sub]]. generalize (subterm_in_instantiated_term _ _ _ Sub). case_eq (subterm_at_pos t1 p). intros u Sub' H. destruct u as [xu | g' lu]. destruct (active_dec (Var xu) (Term f k)) as [Axu_in_k | not_Axu_in_k]. inversion Axu_in_k as [xu' | xu' fk' Axu_in_k']; clear Axu_in_k; subst. rewrite trans_clos_trans_clos_alt in Axu_in_k'; inversion Axu_in_k' as [xu' fk' Axu_in_k | xu' y fk' A1 A2]; subst. apply Acc_l. destruct Axu_in_k as [i [K1 K2]]. rewrite actives_ok; exists i; split; trivial. generalize (nth_error_map (apply_subst sigma) k i); rewrite K2. case (nth_error (map (apply_subst sigma) k) i). intros ti Hi; rewrite H; rewrite Hi; apply eq_refl. contradiction. apply context_acc_subterms_2 with (apply_subst sigma y). apply Acc_l. destruct A2 as [i [K1 K2]]. rewrite actives_ok; exists i; split; trivial. generalize (nth_error_map (apply_subst sigma) k i); rewrite K2. case (nth_error (map (apply_subst sigma) k) i). intros ti Hi; rewrite Hi; apply eq_refl. contradiction. rewrite H; apply instanciated_active_subterm; rewrite <- trans_clos_trans_clos_alt in A1; right; assumption. apply IH. apply Vdp_step with (map (apply_subst sigma) k) (Term g h). left. rewrite H. replace (Term f (map (apply_subst sigma) k)) with (apply_subst sigma (Term f k)); trivial. apply instance; apply Vdp with t1; trivial. rewrite active_is_active; exists p; split; trivial. apply active_position_in_instanciated_term with (Var xu) sigma; trivial. left. intros s s_in_h; apply Acc_h. destruct s_in_h as [i [K1 K2]]. destruct (nth_error_ok_in _ _ K2) as [h1 [h2 [L K3]]]; subst; apply in_or_app; right; left; apply eq_refl. apply refl_trans_clos_is_trans with (Term g h); trivial. right; left; trivial. assert (Dummy : active_subterm (Term g h) (apply_subst sigma t1)). rewrite active_is_active. exists p; split; trivial. assumption. rewrite H. apply IH. apply Cdp_step with (map (apply_subst sigma) k). left. replace (Term f (map (apply_subst sigma) k)) with (apply_subst sigma (Term f k)); trivial. apply instance. apply Cdp with t1; trivial. rewrite active_is_active; exists p; split; trivial. apply active_position_in_instanciated_term with (Term g' lu) sigma; trivial. injection H; clear H; intros; subst; assumption. intros s As; apply Acc_h. rewrite <- H in As; destruct As as [i [K1 K2]]. destruct (nth_error_ok_in _ _ K2) as [h1 [h2 [L K3]]]; subst; apply in_or_app; right; left; apply eq_refl. apply refl_trans_clos_is_trans with (Term g h); trivial. right; left; rewrite H; assumption. assert (Dummy : active_subterm (Term g h) (apply_subst sigma t1)). rewrite active_is_active; exists p; split; trivial. unfold active_subterm in Dummy; assumption. intros Sub' [v [q [q' [J1 [v_in_t1 [Sub'' J2]]]]]]; subst p. destruct (active_dec (Var v) (Term f k)) as [Av_in_k | not_Av_in_k]. apply context_acc_subterms_2 with (apply_subst sigma (Var v)). inversion Av_in_k as [v' | v' fk' Av_in_k']; clear Av_in_k; subst. rewrite trans_clos_trans_clos_alt in Av_in_k'; inversion Av_in_k' as [v' fk' Av_in_k | v' y fk' A1 A2]; subst. apply Acc_l. destruct Av_in_k as [i [K1 K2]]. rewrite actives_ok; exists i; split; trivial. generalize (nth_error_map (apply_subst sigma) k i); rewrite K2. case (nth_error (map (apply_subst sigma) k) i). intros ti Hi; rewrite Hi; apply eq_refl. contradiction. apply context_acc_subterms_2 with (apply_subst sigma y). apply Acc_l. destruct A2 as [i [K1 K2]]. rewrite actives_ok; exists i; split; trivial. generalize (nth_error_map (apply_subst sigma) k i); rewrite K2. case (nth_error (map (apply_subst sigma) k) i). intros ti Hi; rewrite Hi; apply eq_refl. contradiction. apply refl_trans_clos_is_trans with (apply_subst sigma (Var v)). assert (Dummy : active_subterm (Term g h) (apply_subst sigma (Var v))). rewrite active_is_active; exists q'; split; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t1 q sigma). rewrite Sub''; trivial. revert Ap. generalize (apply_subst sigma t1) (apply_subst sigma (Var v)); clear. revert q'; induction q as [ | i q]; simpl. intros q' t s A H; injection H; clear H; intros; subst; trivial. intros q' [v | f l] s. intros; discriminate. case (mem_bool Nat.eqb i (mu f)); [idtac | intros; discriminate]. simpl; case (nth_error l i); [idtac | intros; discriminate]. intro t; apply IHq. left. assert (Dummy : active_subterm (apply_subst sigma (Var v)) (apply_subst sigma y)). apply instanciated_active_subterm; rewrite <- trans_clos_trans_clos_alt in A1; right; assumption. assumption. rewrite active_is_active; exists q'; split; trivial. assert (Sub''' : subterm_at_pos (apply_subst sigma t1) q = Some (apply_subst sigma (Var v))). generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t1 q sigma). rewrite Sub''; trivial. revert Ap Sub'''. generalize (apply_subst sigma t1) (apply_subst sigma (Var v)); clear. revert q'; induction q as [ | i q]; simpl. intros q' t s A H; injection H; clear H; intros; subst; trivial. intros q' [v | f l] s. intros; discriminate. case (mem_bool Nat.eqb i (mu f)); [idtac | intros; discriminate]. simpl; case (nth_error l i); [idtac | intros; discriminate]. intro t; apply IHq. apply IH. apply Vdp_step with (map (apply_subst sigma) k) (apply_subst sigma (Var v)). left. replace (Term f (map (apply_subst sigma) k)) with (apply_subst sigma (Term f k)); trivial. apply instance; apply Vdp with t1; trivial. rewrite active_is_active; exists q; split; trivial. apply active_position_in_instanciated_term with (Var v) sigma; trivial. revert Ap; generalize (apply_subst sigma t1); clear. revert q'; induction q as [ | i q]; intro q'. simpl; trivial. intros [v | f l]. intros; discriminate. simpl; case (mem_bool Nat.eqb i (mu f)); [idtac | intros; discriminate]. case (nth_error l i); [idtac | intros; discriminate]. intros t; simpl; apply IHq. rewrite active_is_active; exists q'; split; trivial. assert (Sub''' : subterm_at_pos (apply_subst sigma t1) q = Some (apply_subst sigma (Var v))). generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t1 q sigma). rewrite Sub''; trivial. revert Ap Sub'''. generalize (apply_subst sigma t1) (apply_subst sigma (Var v)); clear. revert q'; induction q as [ | i q]; simpl. intros q' t s A H; injection H; clear H; intros; subst; trivial. intros q' [v | f l] s. intros; discriminate. case (mem_bool Nat.eqb i (mu f)); [idtac | intros; discriminate]. simpl; case (nth_error l i); [idtac | intros; discriminate]. intro t; apply IHq. intros s s_in_h; apply Acc_h. destruct s_in_h as [i [K1 K2]]. destruct (nth_error_ok_in _ _ K2) as [h1 [h2 [L K3]]]; subst; apply in_or_app; right; left; apply eq_refl. apply refl_trans_clos_is_trans with (Term g h); trivial. right; left; trivial. assert (Dummy : active_subterm (Term g h) (apply_subst sigma t1)). rewrite active_is_active. exists (q ++ q'); split; trivial. assumption. apply (H'' (size (apply_subst sigma t1))). apply le_n. left. apply IHl with (actives f 0 l1); trivial. apply filtering. exists n; split; trivial. intros s H'' H'''; apply IH; trivial. inversion H'' as [f' l1' l2 s' K1 K2 | f' l1' l2 s' K1 K2]; subst. apply Cdp_step with l2; [idtac | trivial]. apply refl_trans_clos_is_trans with l1. assumption. right; left; exists n; split; trivial. apply Vdp_step with l2 s'; [idtac | trivial | trivial]. apply refl_trans_clos_is_trans with l1. assumption. right; left; exists n; split; trivial. intros t H; apply Acc_t. inversion H as [f' l1' l2 s' K1 K2 | f' l1' l2 s' K1 K2]; subst. apply Cdp_step with l2; [idtac | trivial]. apply refl_trans_clos_is_trans with l1. assumption. right; left; exists n; split; trivial. apply Vdp_step with l2 s'; [idtac | trivial | trivial]. apply refl_trans_clos_is_trans with l1. assumption. right; left; exists n; split; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)