proposition: Lemma marked_measure_monotonic : forall f l1 l2, (one_step_list (one_step rules) l2 l1) -> marked_measure (Term f l2) <= marked_measure (Term f l1).
proof: Proof. intros f l1 l2 H. simpl. case (defined_dec f);[intro Hdef|intro Hconst]. apply measure_list_monotonic. assumption. apply Marked_pols_monononic. apply measure_list_monotonic. assumption. apply All_monotonic. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)