proposition: Lemma remove_edge : forall (dpR R : relation term) P u0 v0 (lo so : relation term), (forall t, lo t t) -> (forall t1 t2 t3, lo t1 t2 -> lo t2 t3 -> lo t1 t3) -> (forall t1 t2 t3, so t1 t2 -> lo t2 t3 -> so t1 t3) -> well_founded so -> (forall s t, one_step R s t -> lo s t) -> (forall u v, dpR v u -> forall sigma, lo (apply_subst sigma v) (apply_subst sigma u)) -> (forall sigma, so (apply_subst sigma v0) (apply_subst sigma u0)) -> well_founded (rest P (rdp_step (axiom dpR) R)) -> well_founded (rest P (rdp_step (axiom (union _ (fun s t => (s,t) = (v0,u0)) dpR)) R)).
proof: Proof. intros dpR R P u0 v0 lo so lo_refl lo_trans Transo Wo Hlo Hlo' Hso W. assert (WW := wf_lex _ _ _ Transo Wo W). intro t; apply (well_founded_ind WW); clear t. intros t IH; apply Acc_intro; intros s H; apply IH; clear WW IH. destruct H as [H [Ps Pt]]. inversion H as [f l1 l2 v K1 K2]; clear H; subst. inversion K2 as [v u sigma [K3 | K3]]; clear K2; subst. injection K3; clear K3; intros; subst u v. left; apply Transo with (Term f l2). rewrite <- H0; apply Hso. inversion K1 as [l | k1 k2 K]; clear K1; subst. apply lo_refl. clear Pt H0; induction K as [k1 k2 K | k1 k2 k3 K1 K2]. apply Hlo; apply in_context; assumption. apply lo_trans with (Term f k2); [apply Hlo; apply in_context | ]; assumption. right. apply lo_trans with (Term f l2). rewrite <- H0; apply Hlo'; assumption. inversion K1 as [l | k1 k2 K]; clear K1; subst. apply lo_refl. clear Pt H0; induction K as [k1 k2 K | k1 k2 k3 K1 K2]. apply Hlo; apply in_context; assumption. apply lo_trans with (Term f k2); [apply Hlo; apply in_context | ]; assumption. split; [ constructor 1 with l2; [ | rewrite <- H0; apply instance] | split]; assumption. Qed.
imports: Coq(List Relations Wellfounded Arith Recdef Setoid) CoLoR(closure more_list weaved_relation term_spec equational_theory_spec)