proposition: Lemma P_acc_with_subterm : forall R P t, Acc (P_step R P) t <-> Acc (union _ (P_step R P) direct_subterm) t.
proof: Proof. intros R P 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 (P_step R P) u). apply P_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 (P_acc_with_subterm_subterms R P (Term f (l' ++ v :: l''))). apply IH; apply P_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) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)