proposition: Lemma wf_union : well_founded (Sdp.sdp.Rcdp_min R_rules dps_union).
proof: Proof. apply Sdp.wf_union_Rcdp_rest with (Tle:=rpo_eq_afs) (Tlt:=rpo_afs) (dps:=dps) (dps_large:=dps_large) (inject_symb:=Mrk.inject_symb) (mark_symb:=Mrk.mark_symb); try assumption. unfold rpo_afs; apply Inverse_Image.wf_inverse_image; apply Rpo.wf_rpo; apply (prec_wf prec_union). apply AfsM.Tle_monotone_afs; [ apply Ext.rpo_eq_monotone | constructor; constructor | apply Ext.rpo_eq_trans ]. apply AfsM.Tlt_Tle_compat_afs; apply Ext.rpo_rpo_eq_compat. apply rpo_eq_stable_afs. apply rpo_stable_afs. intros t1 t2 sigma H; unfold Tlt_mark; unfold inject_term; unfold mark_term; rewrite Sdp.mark_inject_subst; [| apply (dps_large_non_variable H) ]; rewrite Sdp.mark_inject_subst; [| apply (dps_large_non_variable H) ]; unfold rpo_eq_afs; unfold afs; rewrite AfsM.afs_subst; rewrite AfsM.afs_subst; apply Rpo.rpo_eq_subst; apply dps_large_decrease; assumption. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)