proposition: Lemma acc_with_subterm : forall R t, Acc (one_step R) t <-> Acc (union _ (one_step R) direct_subterm) t.
proof: Proof. intros R t; split. intro Acc_t; induction Acc_t as [t Acc_t IH]. generalize Acc_t IH; clear Acc_t IH; pattern t; apply term_rec2; clear t. intro n; induction n as [ | n]; intros t size_t Acc_t IH. absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t); trivial; apply size_ge_one. apply Acc_intro. intros u H; destruct H as [H | H]. apply IH; trivial. apply IHn. apply le_S_n; apply Nat.le_trans with (size t); trivial. apply size_direct_subterm; trivial. assert (H' : Acc (one_step R) u). apply acc_subterms_1 with t; trivial. apply Acc_intro; apply Acc_t. inversion H'; trivial. intros v v_R_u. destruct t as [ x | f l]. contradiction. destruct (In_split _ _ H) as [l' [l'' H'']]; clear H; subst l. apply (acc_with_subterm_subterms R (Term f (l' ++ v :: l''))). apply IH; apply one_step_context_in; trivial. simpl; apply in_or_app; right; left; trivial. apply Acc_incl; intros t1 t2 H; left; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith Setoid) CoLoR(closure more_list weaved_relation dickson term_spec equational_theory_spec)