proposition: Lemma length_flatten : forall f, forall l, arity f = AC -> (forall u, In u l -> well_formed u) -> length l <= length (flatten f (map canonical_form l)).
proof: Proof. intros f l; pattern l; apply (list_rec3 size); clear l; induction n; destruct l as [ | t l]. simpl; trivial. simpl; intro S_l; absurd (1 <= 0); auto with arith; apply Nat.le_trans with (size t + list_size size l); trivial. apply Nat.le_trans with (2 := Nat.le_add_r _ _), size_ge_one. simpl; trivial. intros Sl Af Wl; replace (t :: l) with ((t :: nil) ++ l); trivial; rewrite map_app; rewrite flatten_app; do 2 rewrite length_app; apply Nat.add_le_mono. assert (Wt : well_formed t). apply Wl; left; trivial. destruct t as [v | g ll]; simpl; auto with arith. generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intro f_eq_g | intro f_diff_g]. subst g; rewrite <- app_nil_end; rewrite Af; rewrite length_quicksort; apply Nat.le_trans with (length ll). elim (well_formed_unfold Wt); rewrite Af; intros _ Lll; rewrite Lll; auto with arith. apply IHn; trivial. apply le_S_n; apply Nat.le_trans with (size (Term f ll) + list_size size l); trivial; rewrite size_unfold; simpl; apply le_n_S; apply Nat.le_add_r. elim (well_formed_unfold Wt); rewrite Af; trivial. apply le_n. apply IHn; trivial. apply Nat.add_le_mono_l with 1; apply Nat.le_trans with (size t + list_size size l); trivial; apply Nat.add_le_mono_r; apply size_ge_one. intros; apply Wl; right; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)