proposition: Lemma size_size_aux2 : forall f t, arity f = AC -> well_formed t -> ac_size (canonical_form t) = list_size ac_size (flatten f (canonical_form t :: nil)) + (length (flatten f (canonical_form t :: nil))) - 1.
proof: Proof. intros f t Af Wt; assert (Wu : well_formed_cf (canonical_form t)). apply well_formed_cf_is_well_formed_cf_conv; exists t; split; trivial. generalize (canonical_form t) Wu; clear t Wt Wu; intros u Wu. destruct u as [v | g l]; trivial; simpl. simpl; generalize (F.Symb.eq_bool_ok f g); case (F.Symb.eq_bool f g); [intros f_eq_g; subst g | intros f_diff_g]. rewrite Af; rewrite <- app_nil_end; generalize (well_formed_cf_length Af Wu); intro Ll; destruct (length l) as [ | n]. absurd (2 <= 0); auto with arith. rewrite (Nat.add_comm (list_size ac_size l)); simpl; do 2 rewrite Nat.sub_0_r; trivial. simpl; rewrite (list_size_fold ac_size); trivial. simpl; rewrite Nat.add_0_r; apply sym_eq; rewrite Nat.add_comm; simpl; rewrite Nat.sub_0_r; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)