proposition: Lemma bregexp_ceP : forall r1 r2, match bregexp_ce r1 r2 with | None => r1 ≡ r2 | Some s => ((rev s \in r1) && (rev s \notin r2)) \/ ((rev s\notin r1) && (rev s\in r2)) end.
proof: Proof. move => r1 r2. have htemp : gpred_list (ff r1 r2) [:: (r1, r2, [::])]. - rewrite /ff /=. by split. have htemp2: gpred_list (ff r1 r2) (lminus sim_dec3 (DER [::(r1,r2,[::])]) [::(r1,r2,[::])]). - apply: lminus_pred. by apply: DER_preserves_lang. rewrite /bregexp_ce. move: (extract_word_tool (build_list_fun r1 r2)). case: extract_word. - move => a [e [f [h1]]]. rewrite /predC /= => h2. have hpred : gpred_list (ff r1 r2) (build_list_fun r1 r2). + by rewrite /build_list_fun; apply: l4. move: (gpred_listP2 h1 hpred). rewrite /ff => [[hl1 hl2]]. move : (hl1 [::]) (hl2 [::]); clear hl1 hl2. rewrite -!mem_derE !mem_wder /= => -> ->. move : h2. case: (has_eps e) => //=. case: (has_eps f) => //= _; by left. case: (has_eps f) => //= _; by right. - by move/bregexp_eqP. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)