proposition: Lemma dp_criterion_min_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 (dp_step_min R) t -> (forall s, direct_subterm s t -> Acc (one_step R) s) -> Acc (one_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 Acc_var; assumption. simpl in Acc_l; rewrite acc_one_step_list in Acc_l; revert Acc_t IH. induction Acc_l as [l Acc_l IHl]. revert l Acc_l IHl. assert (Main : forall l (Hsub : Acc (one_step_list (one_step R)) l) (IH2 : forall y (Hy : one_step_list (one_step R) y l) (Ht' : Acc (dp_step_min R) (Term f y)) (Hsub' : forall y0, dp_step_min R y0 (Term f y) -> (forall s : term, direct_subterm s y0 -> Acc (one_step R) s) -> Acc (one_step R) y0), Acc (one_step R) (Term f y)) (Ht : Acc (dp_step_min R) (Term f l)) (IH1 : forall y, dp_step_min R y (Term f l) -> (forall s : term, direct_subterm s y -> Acc (one_step R) s) -> Acc (one_step R) y), Acc (one_step R) (Term f l)). intros l Acc_l IH2 Acc_t IH1. apply Acc_intro; intros s H; destruct s as [x1 | f1 l1]. apply Acc_var; assumption. inversion H as [t1 t2 H' | f' 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 -> (exists p, subterm_at_pos t1 p = Some t) -> Acc (one_step R) (apply_subst sigma 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 [p H'']. apply E.var_acc with k. apply (RR _ _ t1_R_t2 x). apply var_in_subterm with (Var x) p; trivial. left; trivial. rewrite acc_one_step_list; assumption. assert (Acc_h : forall t, In t h -> Acc (one_step R) (apply_subst sigma t)). intros t t_in_h; apply IHn. apply le_S_n; refine (Nat.le_trans _ _ _ _ St); apply size_direct_subterm; assumption. destruct (In_split _ _ t_in_h) as [h' [h'' K]]; subst h. exists (p ++ (length h' :: nil)). apply subterm_in_subterm with (Term g (h' ++ t :: h'')). assumption. simpl; rewrite nth_error_at_pos; trivial. destruct (CD g) as [Cg | Dg]. simpl; apply acc_subterms; trivial. intros t t_in_map_h; rewrite in_map_iff in t_in_map_h. destruct t_in_map_h as [t' [H''' t'_in_h]]; subst; apply Acc_h; trivial. apply IH1. split. apply Rdp_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 Dp with t1 p; trivial. split. intros s s_in_h; simpl in s_in_h; rewrite in_map_iff in s_in_h. destruct s_in_h as [_s [_ssig_eq_s _s_in_h]]; subst. apply Acc_h; trivial. unfold acc_sub; simpl; rewrite acc_one_step_list; assumption. intros s s_in_h; simpl in s_in_h. rewrite in_map_iff in s_in_h. destruct s_in_h as [u [H2 u_in_h]]; subst. apply Acc_h; trivial. apply (H'' (size t1)). apply le_n. exists (@nil nat); simpl; trivial. apply IH2; trivial. apply Acc_intro; intros s [H'' [acc_sub_s acc_l1]]. apply Acc_inv with (Term f l); trivial. split; [idtac | split]; trivial. apply one_step_subterm_rdp_rdp with l1; trivial. unfold acc_sub; simpl; rewrite acc_one_step_list; assumption. intros s [H'' [acc_sub_s acc_l1]] _. apply IH1; trivial. split; [idtac | split]; trivial. apply one_step_subterm_rdp_rdp with l1; trivial. unfold acc_sub; simpl; rewrite acc_one_step_list; assumption. intros; apply (Main l). apply Acc_intro; assumption. intros; apply IHl; trivial. intros; apply Acc_inv with (Term f y); assumption. apply Acc_intro; assumption. apply IH. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)