proposition: Lemma marked_measure_star_monotonic : forall f l1 l2, refl_trans_clos (one_step_list (one_step rules)) l2 l1 -> marked_measure (Term f l2) <= marked_measure (Term f l1).
proof: Proof. intros . destruct H as [x | r l H]. apply Aop.(le_refl). induction H. apply marked_measure_monotonic; assumption. apply Aop.(le_trans) with (marked_measure (Term f y)). apply marked_measure_monotonic; assumption. assumption. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)