proposition: Lemma acc_well_formed_acc_all : (forall t, well_formed t -> Acc (one_step R) t) -> forall t, Acc (one_step R) t.
proof: Proof. intros WfR. intro t; pattern t; apply term_rec3; clear t. intros v; apply Acc_intro. intros y H; inversion H as [t1 t2 H1 | ]. subst t1 t2. inversion H1 as [t1 t2 sigma]; subst. destruct t2 as [ | ]; [apply False_rect; apply (R_var _ _ H0) | discriminate]. intros f l Acc_l. destruct (eq_nat_dec (match F.arity f with Free n => n | _ => 2 end ) (length l)) as [L | L]. destruct (decompose_term (Term f l)) as [s [sigma [H0 [Ws [H1 [H2 [H3 H4]]]]]]]. rewrite H0. destruct s as [z | g k]. apply False_rect; revert H0; simpl. case_eq (find X.eq_bool z sigma); [intros z_val z_sig | intro z_sig]; [idtac | discriminate]. intro H0; apply (H1 z (Term f l)). rewrite H0; destruct (find_mem _ _ X.eq_bool_ok _ _ z_sig) as [z' [sig1 [sig2 [z_eq_z' H]]]]; subst z'. rewrite H; apply in_or_app; right; left; trivial. trivial. apply acc_decomposed_term with (map (fun x => apply_subst sigma (Var x)) (var_list (Term g k))); trivial. rewrite <- acc_one_step_list. intros t t_in_sig. rewrite in_map_iff in t_in_sig; destruct t_in_sig as [x [H x_in_s]]. destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x_in_s)) as [p Sub]. destruct p as [ | i p]. discriminate. simpl in Sub; revert Sub; generalize (nth_error_ok_in i k). destruct (nth_error k i) as [ti | ]. intros H'; destruct (H' _ (eq_refl _)) as [l1 [l2 [L' H'']]]. intro Sub; subst t. apply acc_subterms_3 with p (apply_subst sigma ti). apply Acc_l; injection H0; clear H0; intros; subst l. rewrite in_map_iff; exists ti; split; trivial. subst k; apply in_or_app; right; left; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos ti p sigma). rewrite Sub; trivial. intros _ H'; discriminate. intros x u xu_in_sig. assert (x_in_s : In x (var_list (Term g k))). rewrite H4; rewrite in_map_iff; exists (x,u); split; trivial. replace u with (apply_subst sigma (Var x)). destruct (var_in_subterm2 _ _ (in_impl_mem (@eq _) (fun a => eq_refl a) _ _ x_in_s)) as [p Sub]. destruct p as [ | i p]. discriminate. simpl in Sub; revert Sub; generalize (nth_error_ok_in i k). destruct (nth_error k i) as [ti | ]. intros H'; destruct (H' _ (eq_refl _)) as [l1 [l2 [L' H'']]]. intro Sub. apply acc_subterms_3 with p (apply_subst sigma ti). apply Acc_l; injection H0; clear H0; intros; subst l. rewrite in_map_iff; exists ti; split; trivial. subst k; apply in_or_app; right; left; trivial. generalize (subterm_at_pos_apply_subst_apply_subst_subterm_at_pos ti p sigma). rewrite Sub; trivial. intros _ H'; discriminate. simpl. rewrite subst_aux with sigma x u; trivial. intros; rewrite <- H4; trivial. apply almost_const; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)