proposition: Lemma swap_right : 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 -> size a3 <= n -> well_formed a3 -> size a4 <= n -> well_formed a4 -> forall k1 k2 k3, k1 = nil \/ k2 = nil \/ k3 = nil \/ (permut (flatten f (canonical_form a1 :: nil)) (k1 ++ k2) -> permut (flatten f (canonical_form a2 :: nil)) k3 -> permut (flatten f (canonical_form a3 :: nil)) (k1 ++ 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 Sa3 Wa3 Sa4 Wa4 k1 k2 k3. destruct k1 as [ | h1 k1]; [left; trivial | right]; destruct k2 as [ | h2 k2]; [left; trivial | right]; destruct k3 as [ | h3 k3]; [left; trivial | right]; intros P1 P2 P3 P4; generalize (split_cf Af _ _ Wa1 P1); intros [Hk1 | [Hk2 | [t1 [t2 [Wt1 [Wt2 [H1 [Q1 Q2]]]]]]]]; generalize (split_cf Af _ _ Wa3 P3); intros [Hk1' | [Hk3 | [t1' [t3 [Wt1' [Wt3 [H3 [Q1' Q3]]]]]]]]; subst; try discriminate. apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: a2 :: nil)). refine (context_in _ _ _ _ f nil (_ :: nil)); trivial. apply trans_clos_is_trans with (Term f ((Term f (t1 :: t2 :: nil)) :: t3 :: nil)). refine (context_in _ _ _ _ f (_ :: nil) nil). apply IH; trivial; apply flatten_cf_cf with f; trivial; rewrite P2; rewrite Q3; auto. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t2 :: t3 :: nil)) :: nil)). apply l_assoc; trivial. apply trans_clos_is_trans with (Term f (t1 :: (Term f (t3 :: t2 :: nil)) :: nil)). refine (context_in _ _ _ _ f (_ :: nil) nil). apply comm; right; trivial. apply trans_clos_is_trans with (Term f ((Term f (t1 :: t3 :: nil)) :: t2 :: nil)). apply r_assoc; trivial. assert (Wt13 : well_formed (Term f (t1 :: t3 :: nil))). apply well_formed_fold; rewrite Af; split; trivial; intros u [u_eq_t1 | [u_eq_t3 | In_u_nil]]; subst; trivial; contradiction. apply th_sym. apply trans_clos_is_trans with (Term f (Term f (t1 :: t3 :: nil) :: a4 :: nil)). refine (context_in _ _ _ _ f nil (_ :: nil)). apply IH; trivial; apply flatten_cf_cf with f; trivial. rewrite P3; rewrite <- Q1; rewrite <- Q3. rewrite <- flatten_app; simpl; simpl; generalize (F.Symb.eq_bool_ok f f); case (F.Symb.eq_bool f f); [intros _ | intro f_diff_f; apply False_rect; apply f_diff_f; reflexivity]. rewrite Af; rewrite <- app_nil_end; apply quick_permut. refine (context_in _ _ _ _ f (_ :: nil) nil). apply IH; trivial; apply flatten_cf_cf with f; trivial. rewrite P4; rewrite Q2; auto. Qed.
imports: Coq(Setoid Arith List Morphisms) CoLoR(closure more_list weaved_relation list_sort term_spec ac)