proposition: Lemma mkPlusAC_plus_plus_plus: forall l1 l2 l3, wf_re (CPlus l1) -> wf_re (CPlus l2) -> wf_re (CPlus l3) -> mkPlus (mkPlus (CPlus l1) (CPlus l2)) (CPlus l3) = mkPlus (mkPlus (CPlus l1) (CPlus l3)) (CPlus l2).
proof: Proof. move => l1 l2 l3 hw1 hw2 hw3. rewrite !mkPlus_unfold => //. f_equal. apply (@sorted_eq _ cregexp_le). by apply leS_trans. by apply leS_antisym. apply : undup_sorted. by apply leS_trans. apply : merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. apply : undup_sorted. by apply leS_trans. apply : merge_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. apply sort_sorted. by apply leS_total. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_undup !mem_merge !mem_cat !mem_sort. by rewrite orbAC. rewrite -mkPlus_unfold => //. by apply wf_CPlus. rewrite -mkPlus_unfold => //. by apply wf_CPlus. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)