proposition: Lemma measure_strictly_monotonic_aux : forall l2 (IHl2 : forall t : term, In t l2 -> forall r : term, one_step rules r t -> well_formed t -> measure r < measure t), forall l1, one_step_list (one_step rules) l1 l2 -> (forall t, In t l2 -> well_formed t) -> forall n (P1 P2 : Pol_type n), length l2 = n -> monotonic_strict_aux false n P1 P2 -> measure_list l1 n P1 < measure_list l2 n P2.
proof: Proof. intros l IHl k1 H1 Wl. destruct (one_step_in_list H1) as [t1 [t2 [l1 [l2 [K [K1 K2]]]]]]. assert (Ht : measure t2 < measure t1). apply IHl; [idtac | assumption | apply Wl]; subst; apply in_or_app; right; left; apply eq_refl. subst l k1. clear IHl H1 K Wl. induction l1 as [ | a1 l1]; intros [ | n] P1 P2 L Hmon; simpl. discriminate. simpl in P1, P2, Hmon, L; injection L; clear L; intro L. set (P1':=P1 (measure t2)). set (P2':=P2 (measure t1)). assert (Hmon' : monotonic_strict_aux true n P1' P2'). unfold P1', P2'. destruct Hmon as [_ Hmon]. apply Hmon with (x1:=measure t2) (x2:=measure t1). split; [apply measure_bounded | assumption]. clearbody P1'; clearbody P2'. clear P1 P2 Hmon. revert n P1' P2' Hmon' L. induction l2 as [ | t l]; intros n P1 P2 Hmon L. simpl in *; subst n; apply Hmon. destruct n. discriminate L. simpl in *; apply IHl. apply Hmon; split;[apply measure_bounded| apply Aop.(le_refl)]. injection L; intro; assumption. discriminate L. apply IHl1. injection L; intro; assumption. apply Hmon; split;[apply measure_bounded| apply Aop.(le_refl)]. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)