proposition: Lemma l3 : forall (E F:bregexp), forall (X Y:seq (bregexp* bregexp*bword)) (ha: Acc (gpred_list (Prod (set_pair_der E F) bT)) (sup sim3) X) (hp1: gpred_list (Prod (set_pair_ders E F) bT) X) (hp2: gpred_list (Prod (set_pair_ders E F) bT) Y) (hd : ldisjoint sim_dec3 X Y) (hs: sim_incl sim_dec3 (DER X) (X ++ Y)), r_subset sim3 (DER (build_list_fun_acc ha hp1 hp2 hd)) (build_list_fun_acc ha hp1 hp2 hd).
proof: Proof. move => E F X Y ha. move: Y. elim ha using Acc_rect_dep. clear X ha. move => X hp hi [ | hdY tlY] hp1 hp2 /=. - rewrite cats0 => _ hs. by apply/(@sim_inclP _ _ _ sim_dec3). - move => hd hs. apply: hi. apply: (@sim_incl_trans _ _ _ _ (DER X ++ DER (hdY :: tlY))) => /=. by apply: DER_cat. rewrite sim_incl_cat. apply/andP; split. by apply: sim_incl_cat2l. by rewrite lminus_incl. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)