proposition: Lemma ddp_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 (ddp_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 IH. apply dp_criterion_min_local; trivial. clear IH; induction Acc_t as [t Acc_t IH]. apply Acc_intro. intros s [H [Hs Ht]]. inversion H as [f l1 l2 t' K1 K2]; clear H; subst. inversion K2 as [s1 t2 sigma K3]; clear K2; subst. inversion K3 as [l r p g k1 K4 Sub Dg]; clear K3; subst. destruct (subterm_at_pos_dec t2 (Term g k1)) as [[q Sub'] | not_Sub]. destruct q as [ | i q]. absurd (Acc (ddp_step_min R) (Term f l2)). apply cycle_not_acc; split; [idtac | split; trivial]. apply Rdp_step with l2; trivial. left. rewrite <- H0; apply instance. simpl in Sub'; injection Sub'; clear Sub'; intro Sub'; subst t2. split. apply Dp with r p; trivial. intros i q Sub''; generalize (size_subterm_at_pos (Term g k1) i q); rewrite Sub''; apply Nat.lt_irrefl. refine (rwr_sub_acc_sub_acc_sub R l1 l2 K1 Ht). refine (rwr_sub_acc_sub_acc_sub R l1 l2 K1 Ht). apply Acc_intro; intros u [H [Hu Hfl2]]; apply Acc_inv with (Term f l1). apply Acc_intro; assumption. split; [idtac | split; assumption]. apply rwr_subterm_rdp_rdp with l2; trivial. apply Acc_incl with (dp_step R). intros s1 s2 [H _]; assumption. apply acc_one_step_acc_dp; [apply HR | idtac]. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos t2 (i :: q) sigma). rewrite Sub'; rewrite H0; simpl subterm_at_pos. generalize (nth_error_ok_in i l2); destruct (nth_error l2 i) as [ti | ]. intros H Sub''; destruct (H _ (eq_refl _)) as [l2' [l2'' [L2 H']]]; clear H. apply acc_subterms_3 with q ti; trivial. apply (rwr_sub_acc_sub_acc_sub R _ _ K1 Ht); subst l2; apply in_or_app; right; left; apply eq_refl. intros _ H; discriminate. apply IH; split; [idtac | split; trivial]. apply Rdp_step with l2; trivial. rewrite <- H0; apply instance. split; [apply Dp with r p | idtac]; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term equational_theory_spec) CoLoR(NatCompat)