proposition: Lemma commutativity : forall n, (forall t1, size t1 <= n -> forall t2, well_formed t1 -> well_formed t2 -> canonical_form t1 = canonical_form t2 -> ac t1 t2) -> forall f, arity f = AC -> forall a1 a2 a3 a4, size a1 <= n -> well_formed a1 -> size a2 <= n -> well_formed a2 -> well_formed a3 -> well_formed a4 -> forall k2 k3, permut (flatten f (canonical_form a1 :: nil)) k2 -> permut (flatten f (canonical_form a2 :: nil)) k3 -> permut (flatten f (canonical_form a3 :: nil)) k3 -> permut (flatten f (canonical_form a4 :: nil)) k2 -> ac (Term f (a1 :: a2 :: nil)) (Term f (a3 :: a4 :: nil)).
proof: Proof. intros n IH f Af a1 a2 a3 a4 Sa1 Wa1 Sa2 Wa2 Wa3 Wa4 k2 k3 P1 P2 P3 P4. apply trans_clos_is_trans with (Term f (a2 :: a1 :: nil)). apply comm; right; trivial. apply trans_clos_is_trans with (Term f (a3 :: a1 :: nil)). refine (context_in _ _ _ _ f nil (a1 :: nil)). apply IH; trivial; apply flatten_cf_cf with f; trivial; rewrite P2; rewrite P3; auto. refine (context_in _ _ _ _ f (a3 :: nil) nil). apply IH; trivial; apply flatten_cf_cf with f; trivial; rewrite P1; rewrite P4; auto. Qed.
imports: Coq(Setoid Arith List Morphisms) CoLoR(closure more_list weaved_relation list_sort term_spec ac)