proposition: Lemma ssublr_trans : forall y x z, (ssubl x y -> ssubl y z -> ssubl x z) /\ ( ssubr x y -> ssubr y z -> ssubr x z).
proof: Proof. move => y x. elim : x y => [ | | | u | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] //. - move => y z. rewrite !ssublVoid. split; first trivial. by apply ssubr_transV. - elim => [ | | | v | c _ | c1 hc1 c2 hc2 | c1 _ c2 _ | c1 _ c2 _ | c _ ] z //. + split; first done. by apply ssubr_transE. case: (hc1 z) (hc2 z) => h11 h12 [h21 h22]; split. + rewrite ssublPlus1 // ssublPlus2. case/orP => hu; case/andP => h1 h2; [ by apply: h11 | by apply: h21]. by apply ssubr_transE. - elim => [ | | | v | c _ | c1 hc1 c2 hc2 | c1 _ c2 _ | c1 _ c2 _ | c _ ] z //. + split; first done. by apply ssubr_transD. case: (hc1 z) (hc2 z) => hc11 hc12 [hc21 hc22]; split. + rewrite ssublPlus1 // ssublPlus2. case/orP => hu; case/andP => h1 h2; [ by apply: hc11 | by apply: hc21]. by apply ssubr_transD. - elim => [ | | | v | c _ | c1 hc1 c2 hc2 | c1 _ c2 _ | c1 _ c2 _ | c _ ] z //. + split; first done. by apply ssubr_transA. + by split; [ rewrite [ssubl (Atom _) (Atom _)]/= => heq; rewrite (eqP heq) | rewrite [ssubr (Atom _) (Atom _)]/= => heq; rewrite (eqP heq)]. case: (hc1 z) (hc2 z) => hc11 hc12 [hc21 hc22]; split. + rewrite ssublPlus1 // ssublPlus2. case/orP => hu; case/andP => h1 h2; [ by apply: hc11 | by apply: hc21]. by apply ssubr_transA. - elim => [ | | | v | c' hc' | c'1 hc'1 c'2 hc'2 | c'1 _ c'2 _ | c'1 _ c'2 _ | c' _ ] //. + split; first done. elim : z => // r1 hr1 r2 hr2 _. rewrite !ssubrPlus2; case/andP => h1 h2. by rewrite hr1 // hr2. + rewrite ssublStar ssubrStar. elim => //. * move => c''; rewrite !ssublStar !ssubrStar => [[h11 h12]]. by apply: hc. move => r1 [hr11 hr12] r2 [hr21 hr22]. split. * rewrite !ssublPlus1 // => h1. case/orP => hu; apply/orP; [ left; by apply hr11 | right; by apply hr21]. rewrite !ssubrPlus2 => h1. case/andP => h2 h3. by rewrite hr12 // hr22. move => z; rewrite ssublPlus1 // ssublPlus2 ssubrPlus2. split. + case/orP => hu; case/andP => h1 h2; [ by apply hc'1 | by apply hc'2]. case/andP => h1 h2. elim : z => [ | | | v | c' _ | c1' hc1' c2' hc2' | c1' _ c2' _ | c1' _ c2' _ | c' _ ] //; try by( rewrite ssubrPlus1 //; case/orP => hu; [apply hc'1 | apply hc'2] ). rewrite !ssubrPlus2; case/andP => h3 h4. by rewrite hc1' // hc2'. - move => y z; split. + case: (hc1 y z) (hc2 y z) => hy1 _ [hz1 _]. clear hc1 hc2 . elim : y hy1 hz1 => [ | | | v | c' _ | c'1 hc'1 c'2 hc'2 | c'1 _ c'2 _ | c'1 _ c'2 _ | c' _ ] hy1 hz1; rewrite !ssublPlus2; case/andP => h1 h2 h; by rewrite (hy1 h1) // (hz1 h2). have h1 : forall y z, ssubr c1 y -> ssubr y z -> ssubr c1 z. + by apply hc1. have h2 : forall y z, ssubr c2 y -> ssubr y z -> ssubr c2 z. + by apply hc2. clear hc1 hc2. move : z. elim : y => [ | | | v | c' _ | c'1 hc'1 c'2 hc'2 | c'1 _ c'2 _ | c'1 _ c'2 _ | c' _ ]z ; try ( by rewrite ssubrPlus1 //; case/orP => hu h; [ apply ssubrPlusl; apply (h1 _ _ hu) | apply ssubrPlusr; apply (h2 _ _ hu)]). rewrite !ssubrPlus2; case/andP => h3 h4. elim : z => [ | | | v | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] ; try( by rewrite ssubrPlus1 //; case/orP => hu; [apply hc'1 | apply hc'2] ). rewrite !ssubrPlus2; case/andP => g3 g4. by rewrite hd1 // hd2. - elim => [ | | | v | c' hc' | c'1 hc'1 c'2 hc'2 | c'1 _ c'2 _ | c'1 _ c'2 _ | c' _ ] //. + split; first done. elim : z => // r1 hr1 r2 hr2 _. rewrite !ssubrPlus2; case/andP => h1 h2. by rewrite hr1 // hr2. + move => z; rewrite ssublPlus1 // ssublPlus2 ssubrPlus2. split. * case/orP => hu; case/andP => h1 h2; [ by apply hc'1 | by apply hc'2]. case/andP => h1 h2. elim : z => [ | | | v | c' _ | c1' hc1' c2' hc2' | c1' _ c2' _ | c1' _ c2' _ | c' _ ] //; try by( rewrite ssubrPlus1 //; case/orP => hu; [apply hc'1 | apply hc'2] ). rewrite !ssubrPlus2; case/andP => h3 h4. by rewrite hc1' // hc2'. rewrite ssublAnd ssubrAnd. elim => //. + move => r1 [hr11 hr12] r2 [hr21 hr22]; split. * rewrite !ssublPlus1 // => h1. case/orP => hu; apply/orP; [ left; by apply hr11 | right; by apply hr21]. rewrite !ssubrPlus2 => h1. case/andP => h2 h3. by rewrite hr12 // hr22. move => r1 [hr11 hr12] r2 [hr21 hr22]. split; case/andP => h1 h2. + rewrite !ssublAnd; case/andP => h3 h4. by apply/andP; split; [apply (hc1 c'1 r1) | apply (hc2 c'2 r2)]. rewrite !ssubrAnd; case/andP => h3 h4. by apply/andP; split; [apply (hc1 c'1 r1) | apply (hc2 c'2 r2)]. - elim => [ | | | v | c' hc' | c'1 hc'1 c'2 hc'2 | c'1 _ c'2 _ | c'1 _ c'2 _ | c' _ ] //. + split; first done. elim : z => // r1 hr1 r2 hr2 _. rewrite !ssubrPlus2; case/andP => h1 h2. by rewrite hr1 // hr2. + move => z; rewrite ssublPlus1 // ssublPlus2 ssubrPlus2. split. * case/orP => hu; case/andP => h1 h2; [ by apply hc'1 | by apply hc'2]. case/andP => h1 h2. elim : z => [ | | | v | c' _ | c1' hc1' c2' hc2' | c1' _ c2' _ | c1' _ c2' _ | c' _ ] //; try by( rewrite ssubrPlus1 //; case/orP => hu; [apply hc'1 | apply hc'2] ). rewrite !ssubrPlus2; case/andP => h3 h4. by rewrite hc1' // hc2'. rewrite ssublConc ssubrConc. elim => //. + move => r1 [hr11 hr12] r2 [hr21 hr22]; split. * rewrite !ssublPlus1 // => h1. case/orP => hu; apply/orP; [ left; by apply hr11 | right; by apply hr21]. rewrite !ssubrPlus2 => h1. case/andP => h2 h3. by rewrite hr12 // hr22. move => r1 [hr11 hr12] r2 [hr21 hr22]. split; case/andP => h1 h2. + rewrite !ssublConc; case/andP => h3 h4. by apply/andP; split; [apply (hc1 c'1 r1) | apply (hc2 c'2 r2)]. rewrite !ssubrConc; case/andP => h3 h4. by apply/andP; split; [apply (hc1 c'1 r1) | apply (hc2 c'2 r2)]. elim => [ | | | v | c' hc' | c'1 hc'1 c'2 hc'2 | c'1 _ c'2 _ | c'1 _ c'2 _ | c' _ ] //. - split; first done. elim : z => // r1 hr1 r2 hr2 _. rewrite !ssubrPlus2; case/andP => h1 h2. by rewrite hr1 // hr2. - move => z; rewrite ssublPlus1 // ssublPlus2; split. * case/orP => hu; case/andP => h1 h2; [ by apply hc'1 | by apply hc'2]. rewrite ssubrPlus2; case/andP => h1 h2. elim : z => [ | | | v | c' _ | c1' hc1' c2' hc2' | c1' _ c2' _ | c1' _ c2' _ | c' _ ] //; try by( rewrite ssubrPlus1 //; case/orP => hu; [apply hc'1 | apply hc'2] ). rewrite !ssubrPlus2; case/andP => h3 h4. by rewrite hc1' // hc2'. move => z. rewrite ssublNot ssubrNot. elim :z => //. - move => r1 [hr11 hr12] r2 [hr21 hr22]. split => h1. + rewrite !ssublPlus1 //. case/orP => hu; apply/orP; [left; by apply hr11 | right; by apply hr21]. rewrite !ssubrPlus2; case/andP => h2 h3. by rewrite hr12 // hr22. move => r [hr1 hr2]; rewrite !ssublNot !ssubrNot. split => h1 h2. - by apply (hc c' r). by apply (hc c' r). Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(regexp finite_der equiv)