proposition: Lemma measure_strictly_monotonic : forall l r, (EQT.one_step rules r l) -> well_formed l -> measure r < measure l.
proof: 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_strictly_monotonic; assumption. intros f l IHl r H W. inversion H as [t1 t2 H1 | g k1 k2 H1 H2 H3]; clear H; subst. apply rules_strictly_monotonic; assumption. assert (L : length l = get_arity f). unfold well_formed in W; simpl in W; rewrite Bool.andb_true_iff in W; destruct W as [_ W]. apply Nat.eqb_eq; unfold get_arity; destruct (arity f) as [ | | n]; assumption. apply measure_strictly_monotonic_aux; trivial. apply (well_formed_unfold W). generalize (All_strictly_monotonic f); set (f_pol:=Pols f). clearbody f_pol. revert f_pol. rewrite <- L. revert H1; case l; [intro H1; inversion H1 | intros a1 l1 _; intros; assumption]. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)