proposition: Lemma ac_size_build_lt_args : forall f l1 l2 t1, arity f = AC -> well_formed_cf (Term f (l1 ++ t1 :: l2)) -> ac_size (build f (l1 ++ l2)) + ac_size t1 < ac_size (Term f (l1 ++ t1 :: l2)).
proof: Proof. intros f l1 l2 t1 Ar W; pattern (ac_size (Term f (l1 ++ t1 :: l2))); rewrite ac_size_unfold. rewrite ac_size_build_eq; trivial. do 2 rewrite length_app; do 2 rewrite list_size_app; simpl; rewrite <- Nat.add_assoc; apply Nat.add_lt_le_mono. rewrite (Nat.add_comm (length l1) (S (length l2))); simpl; rewrite <- Nat.sub_0_r; rewrite (Nat.add_comm (length l2)); elim W; clear W; rewrite Ar; intros _ W; elim W; clear W; intros L _; rewrite length_app in L; simpl in L; rewrite Nat.add_comm in L; simpl in L; rewrite Nat.add_comm in L; destruct (length l1 + length l2). absurd (1 >= 2); trivial; unfold ge; auto with arith. auto with arith. rewrite <- Nat.add_assoc; apply Nat.add_le_mono_l; rewrite Nat.add_comm; auto with arith. Qed.
imports: Coq(Arith List) CoLoR(more_list list_sort term_spec ac cf_eq_ac matching)