proposition: Lemma wf_CConc : forall r1 r2, wf_re r1 -> wf_re r2 -> wf_re (mkConc r1 r2).
proof: Proof. move => r1. case: (toolmkConc r1). - by move => heq r2; rewrite (eqP heq) mkConc_CVoid_lt. - by move => heq r2; rewrite (eqP heq) mkConc_CEps_lt. - case => l heq r2; rewrite (eqP heq) /=;clear heq r1. case/andP => h1 h2. case: (toolmkConc r2). * by move => heq; rewrite (eqP heq). * move => heq _; rewrite (eqP heq). by apply/andP; split. * case => l' heq; rewrite (eqP heq) /=; clear heq r2. case/andP => h3 h4. apply/andP; split. rewrite size_cat /=. by apply ltn_addl. by rewrite all_cat h2 h4. * case. case: r2 => [ | | | t | d | k | k | k | d ] //=. + move => _ _ _ hr2. apply/andP; split. rewrite size_cat /=; change 1 with (0+1); rewrite ltn_add2r; by apply (@ltn_trans 1). by rewrite all_cat /= andbT. + move => _ _ _ hr2. apply/andP; split. rewrite size_cat /=; change 1 with (0+1); rewrite ltn_add2r; by apply (@ltn_trans 1). by rewrite all_cat andbT. + move => _ _ _ hr2. apply/andP; split. rewrite size_cat /=; change 1 with (0+1); rewrite ltn_add2r; by apply (@ltn_trans 1). by rewrite all_cat h2 /= andbT. + move => _ _ _ hr2. apply/andP; split. rewrite size_cat /=; change 1 with (0+1); rewrite ltn_add2r; by apply (@ltn_trans 1). by rewrite all_cat h2 /= andbT. + move => _ _ _ hr2. apply/andP; split. rewrite size_cat /=; change 1 with (0+1); rewrite ltn_add2r; by apply (@ltn_trans 1). by rewrite all_cat h2 /= andbT. + move => _ _ h. move/negP : (h k); by case. + move => _ _ _ hr2. apply/andP; split. rewrite size_cat /=; change 1 with (0+1); rewrite ltn_add2r; by apply (@ltn_trans 1). by rewrite all_cat h2 /= andbT. - move => hr1 r2 hw1. case: (toolmkConc r2). * by move => heq; rewrite (eqP heq) mkConc_CVoid_rt. * by move => heq; rewrite (eqP heq) mkConc_CEps_rt. * case => l heq; rewrite (eqP heq) /=; clear r2 heq. case/andP => h1 h2. rewrite mkConc_unfold2 => //=. rewrite h2 hw1 !andbT. by apply (@ltn_trans (size l)). * move => hr2 hw2. rewrite mkConc_unfold3 => //=. by rewrite hw1 hw2. 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)