proposition: Lemma measure_monotonic : forall l r, (EQT.one_step rules r l) -> measure r <= measure l.
proof: Proof. intro l; pattern l; apply term_rec3; clear l. intros v r H; inversion H as [t1 t2 H1 | ]; clear H; subst. apply rules_monotonic; assumption. intros f l IHl r H. inversion H as [t1 t2 H1 | g k1 k2 H1 H2 H3]; clear H; subst. apply rules_monotonic; assumption. assert (IH : forall n (P1 P2 : Pol_type n), monotonic_aux n P1 P2 -> measure_list k1 n P1 <= measure_list l n P2). apply measure_monotonic_aux; trivial. simpl; apply IH; apply All_monotonic. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)