proposition: Lemma wf : well_founded (Sdp.sdp.Rcdp_min R_rules dps).
proof: Proof. apply Sdp.wf_Rcdp_rest with (Tle:=rpo_eq_afs) (Tlt:=rpo_afs) (inject_symb:=Mrk.inject_symb) (mark_symb:=Mrk.mark_symb). 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. Qed.
imports: Coq(Setoid List Relations Lia Arith) CoLoR(weaved_relation list_permut terminaison)