proposition: Lemma ac_syntactic_aux : forall (l1 l2 l3 l4 : list elt), list_permut (l1 ++ l2) (l3 ++ l4) -> (exists u1, exists u2, exists u3, exists u4, list_permut l1 (u1 ++ u2) /\ list_permut l2 (u3 ++ u4) /\ list_permut l3 (u1 ++ u3) /\ list_permut l4 (u2 ++ u4)).
proof: Proof. induction l1. intros l2 l3 l4 P; exists (nil : list elt); exists (nil : list elt); exists l3; exists l4; simpl; intuition. intros l2 l3 l4 P; rewrite <- app_comm_cons in P; elim (in_app_or l3 l4 a (cons_permut_in P)); intro In_a; generalize (split_list_app_cons eq_elt_dec a _ In_a). destruct (split_list eq_elt_dec l3 a); intro; subst l3; rewrite app_ass in P; rewrite <- app_comm_cons in P; generalize (list_permut_remove_hd _ _ P); clear P; intro P; rewrite <- app_ass in P; elim (IHl1 l2 (l ++ l0) l4 P); clear IHl1 P; intros u1 H; elim H; clear H; intros u2 H; elim H; clear H; intros u3 H; elim H; clear H; intros u4 P; elim P; clear P; intros P1 P; elim P; clear P; intros P2 P; elim P; clear P; intros P3 P4; exists (a :: u1); exists u2; exists u3; exists u4; intuition; simpl; trivial. apply context_list_permut_cons; trivial. apply list_permut_sym; apply list_permut_add_cons_inside; apply list_permut_sym; trivial. destruct (split_list eq_elt_dec l4 a); intro; subst l4; rewrite <- app_ass in P; generalize (list_permut_remove_hd _ _ P); clear P; intro P; rewrite app_ass in P; elim (IHl1 l2 l3 (l ++ l0) P); clear IHl1 P; intros u1 H; elim H; clear H; intros u2 H; elim H; clear H; intros u3 H; elim H; clear H; intros u4 P; elim P; clear P; intros P1 P; elim P; clear P; intros P2 P; elim P; clear P; intros P3 P4; exists u1; exists (a :: u2); exists u3; exists u4; intuition; simpl; trivial. apply list_permut_add_cons_inside; trivial. apply list_permut_sym; apply list_permut_add_cons_inside; apply list_permut_sym; trivial. Qed.
imports: decidable_set List more_list Multiset Arith Setoid