proposition: Lemma var_P_acc : forall R P l x sigma, In x (var_list_list l) -> (forall t, In t (map (apply_subst sigma) l) -> Acc (P_step R P) t) -> Acc (P_step R P) (apply_subst sigma (Var x)).
proof: Proof. intros R P l; pattern l; apply (list_rec3 size); clear l; intro n; induction n as [ | n]; intros [ | t l] Sl x sigma H Acc_l. simpl in H; contradiction. simpl in Sl; absurd (1 <= 0); auto with arith. apply Nat.le_trans with (size t). apply size_ge_one. refine (Nat.le_trans _ _ _ _ Sl); auto with arith. simpl in H; contradiction. assert (Sl' : list_size size l <= n). apply le_S_n; refine (Nat.le_trans _ _ _ _ Sl); simpl; apply (Nat.add_le_mono_r 1 (size t) (list_size size l)); apply size_ge_one. destruct t as [y | g k]. simpl in H; destruct H as [y_eq_x | x_in_l]. subst y; apply Acc_l; simpl map; left; trivial. apply (IHn l); trivial; intros; apply Acc_l; simpl map; right; trivial. assert (Sk : list_size size k <= n). apply le_S_n; refine (Nat.le_trans _ _ _ _ Sl); simpl; rewrite (list_size_fold size k); apply le_n_S; apply Nat.le_add_r. assert (Acc_k : forall t, In t (map (apply_subst sigma) k) -> Acc (P_step R P) t). intros t H'; apply P_acc_subterms_1 with (Term g (map (apply_subst sigma) k)). apply Acc_l; simpl map; left; trivial. trivial. replace (var_list_list (Term g k :: l)) with (var_list (Term g k) ++ var_list_list l) in H; trivial. rewrite var_list_unfold in H. generalize (IHn _ Sk x sigma). destruct (in_app_or _ _ _ H) as [x_in_k | x_in_l]. clear H; intro H; generalize (H x_in_k); clear H; intro H; apply H. intros t H'; apply Acc_k; trivial. simpl in H; intros _; apply (IHn l); trivial. intros t H'; apply Acc_l; right; trivial. Qed.
imports: Coq(List Relations Wellfounded Arith) CoLoR(closure decidable_set more_list weaved_relation term_spec equational_theory_spec dp rpo)