proposition: Lemma mkAndAC_nand_nand_and : forall r1 r2 l3, wf_re r1 -> wf_re r2 -> wf_re (CAnd l3) -> [/\ r1 != CVoid , r1 != CNot CVoid & (forall l, r1 != CAnd l)] -> [/\ r2 != CVoid , r2 != CNot CVoid & (forall l, r2 != CAnd l)] -> mkAnd (mkAnd r1 r2) (CAnd l3) = mkAnd (mkAnd r1 (CAnd l3)) r2.
proof: Proof. move => r1 r2 l3 hw1 hw2 hw3 hh1 hh2. rewrite (@toolmkAnd3 r1 r2) => //. rewrite (@mkAnd_unfold3 _ r1) => //. rewrite (@mkAnd_unfold2 _ r2) => //. case_eq (compare r1 r2) => heq. - rewrite mkAnd_unfold3 => //. 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 undup_sorted. by apply leS_trans. apply merge_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. rewrite mem_undup mem_merge mem_cat !mem_sort !mem_seq1. rewrite (compare_eq_axiom heq). by rewrite orbAC orbb. - rewrite mkAnd_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. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort. rewrite mem_seq2 mem_undup mem_merge mem_cat !mem_sort !mem_seq1. by rewrite orbAC. rewrite wf_re_CAnd /=. apply/and4P; split. rewrite andbT. apply/negP; rewrite mem_seq1 => heq2. move :heq. rewrite (eqP heq2). by rewrite compare_refl. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq. by rewrite hw1. by rewrite andbT. - rewrite mkAnd_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. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort. rewrite mem_seq2 mem_undup mem_merge mem_cat !mem_sort !mem_seq1. by rewrite orbAC orbC orbA orbAC. rewrite wf_re_CAnd /=. apply/and4P; split. rewrite andbT. apply/negP; rewrite mem_seq1 => heq2. move :heq. rewrite (eqP heq2). by rewrite compare_refl. rewrite andbT. move : heq ; rewrite /cregexp_le /leS /cmpS /= compare_neg. by case_eq (compare r2 r1). by rewrite hw2. by rewrite andbT. move: hw3. rewrite !wf_re_CAnd. case/and4P => h3 h4 h5. move/allP => h6. apply/and4P; split. apply (@leq_trans (size l3)). done. rewrite (@perm_size _ (undup (merge' [::r1] (sort' l3))) (undup ([::r1]++l3))). rewrite -{1}(@undup_id _ l3). by apply tool_undup_size. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup mem_merge !mem_cat mem_sort !mem_seq1. by apply undup_uniq. apply undup_sorted. by apply leS_trans. apply merge_sorted. by apply leS_total. done. apply sort_sorted. by apply leS_total. apply/allP => x. rewrite mem_undup mem_merge mem_cat mem_sort mem_seq1. case/orP => hu. by rewrite (eqP hu). by apply : h6. 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)