proposition: Lemma measure_monotonic_aux : forall l (IHl : forall t : term, In t l -> forall r : term, one_step rules r t -> measure r <= measure t) k1, one_step_list (one_step rules) k1 l -> forall n (P1 P2 : Pol_type n), monotonic_aux n P1 P2 -> measure_list k1 n P1 <= measure_list l n P2.
proof: Proof. intros l IHl k1 H1. destruct (one_step_in_list H1) as [t1 [t2 [l1 [l2 [K [K1 K2]]]]]]. assert (Ht : measure t2 <= measure t1). apply IHl; [subst; apply in_or_app; right; left; apply eq_refl | assumption]. subst l k1. clear IHl H1 K. induction l1 as [ | a1 l1]; intros [ | n] P1 P2 Hmon; simpl. apply Aop.(le_refl). simpl in P1, P2, Hmon. set (P1':=P1 (measure t2)). set (P2':=P2 (measure t1)). assert (Hmon':monotonic_aux n P1' P2'). unfold P1', P2'. 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'. induction l2 as [|t l];intros n P1 P2 Hmon. simpl. destruct n. simpl in *. apply Hmon. apply Aop.(le_refl). simpl. destruct n. apply Aop.(le_refl). apply IHl. apply Hmon. split;[apply measure_bounded| apply Aop.(le_refl)]. apply Aop.(le_refl). apply IHl1; trivial. simpl in P1, P2, Hmon. apply Hmon. split;[apply measure_bounded| apply Aop.(le_refl)]. Qed.
imports: Coq(List ZArith Lia) CoLoR(weaved_relation equational_theory term_spec terminaison)