proposition: Lemma finite_number_of_der: forall e, Finite (set_of_der e).
proof: Proof. elim => [ | | | s | c1 hc1 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 ] /=. - apply: cBar => c. case => [ss]. rewrite wder_Void /sim => hVoid. apply cBar => [x]. case. case => [tt]. rewrite wder_Void /sim => hVoid2. case. rewrite /sim . transitivity (Void char) => //. by symmetry. - apply: cBar => c. case => [ss]. case : (wder_Eps ss) => ->. * move => hsim. apply cBar => [x]. case. case => [ tt ]. case: (wder_Eps tt) => ->. + move => hsim2. case. rewrite /sim . transitivity (Eps char) => //; by symmetry. + move => hsim2 _. apply cBar => [x']. case => [] [[tt']]. case: (wder_Eps tt') => ->; move => hsim3. case. transitivity (Eps char) =>//; by symmetry. move => _; case. transitivity (Void char) =>//; by symmetry. * move => hsim1. apply cBar => [x]. case. case => [ tt ]. case: (wder_Eps tt) => ->. + move => hsim2 _ . apply cBar => [x']. case => [] [[tt']]. case: (wder_Eps tt') => ->; move => hsim3. move => _; case. transitivity (Eps char) => //. by symmetry. case. transitivity (Void char) => //. by symmetry. + move => hsim2. case. transitivity (Void char) => //. by symmetry. - apply: cBar => c; case => [ss]. case : (wder_Dot ss) => [ -> | [ -> | ->]]. * move => h1. apply cBar => [x]. case. case => [tt]. case : (wder_Dot tt) => [ -> | [ -> | -> ]]. move => h2. + case. transitivity (Dot char) => //; by symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Dot uu) => [ -> | [ -> | -> ]]. move => h3. case. by transitivity (Dot char) => //; symmetry. move => h3 _. case. by transitivity (Eps char) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Dot vv) => [ -> | [ -> | -> ]]. move => h4. case. by transitivity (Dot char) =>//; symmetry. move => h4 _ . case. by transitivity (Eps char) => //; symmetry. move => h4 _ _ . case. by transitivity (Void char) =>//; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Dot uu) => [ -> | [ -> | -> ]]. move => h3. case. by transitivity (Dot char) =>//; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Dot vv) => [ -> | [ -> | -> ]]. move => h4. case. by transitivity (Dot char) => //; symmetry. move => h4 _ _ . case. by transitivity (Eps char) => //; symmetry. move => h4 _ . case. by transitivity (Void char) => //; symmetry. move => h3 _. case. by transitivity (Void char) => //; symmetry. * move => h1; apply cBar => [x]. case. case => [tt]. case : (wder_Dot tt) => [ -> | [ -> | -> ]]. move => h2. + move => _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Dot uu) => [ -> | [ -> | -> ]]. move => h3 _. case. by transitivity (Dot char) => //; symmetry. move => h3. case. by transitivity (Eps char) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Dot vv) => [ -> | [ -> | -> ]]. move => h4 _. case. by transitivity (Dot char) => //; symmetry. move => h4 . case. by transitivity (Eps char) =>//; symmetry. move => h4 _ _ . case. by transitivity (Void char)=>//; symmetry. + move => h2. case. by transitivity (Eps char) => //; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Dot uu) => [ -> | [ -> | -> ]]. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Dot vv) => [ -> | [ -> | -> ]]. move => h4 _ _. case. by transitivity (Dot char) => //; symmetry. move => h4 . case. by transitivity (Eps char) => //; symmetry. move => h4 _ . case. by transitivity (Void char) => //; symmetry. move => h3. case. by transitivity (Eps char) => //; symmetry. move => h3 _. case. by transitivity (Void char) => //; symmetry. * move => h1; apply cBar => [x]. case. case => [tt]. case : (wder_Dot tt) => [ -> | [ -> | -> ]]. move => h2. + move => _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Dot uu) => [ -> | [ -> | -> ]]. move => h3 _. case. by transitivity (Dot char) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Dot vv) => [ -> | [ -> | -> ]]. move => h4 _. case. by transitivity (Dot char) => //; symmetry. move => h4 _ _ . case. by transitivity (Eps char) => //; symmetry. move => h4 . case. by transitivity (Void char) => //; symmetry. move => h3. case. by transitivity (Void char) => //; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Dot uu) => [ -> | [ -> | -> ]]. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Dot vv) => [ -> | [ -> | -> ]]. move => h4 _ _. case. by transitivity (Dot char) => //; symmetry. move => h4 _ . case. by transitivity (Eps char) => //; symmetry. move => h4 . case. by transitivity (Void char) => //; symmetry. move => h3 _. case. by transitivity (Eps char) => //; symmetry. move => h3. case. by transitivity (Void char) => //; symmetry. + move => h2. case. by transitivity (Void char) => //; symmetry. - apply: cBar => c; case => [ss]. case : (wder_Atom ss s) => [ -> | [ -> | ->]]. * move => h1. apply cBar => [x]. case. case => [tt]. case : (wder_Atom tt s) => [ -> | [ -> | -> ]]. move => h2. + case. by transitivity (Atom s) => //; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Atom uu s) => [ -> | [ -> | -> ]]. move => h3. case. by transitivity (Atom s) => //; symmetry. move => h3 _. case. by transitivity (Eps char) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Atom vv s) => [ -> | [ -> | -> ]]. move => h4. case. by transitivity (Atom s) => //; symmetry. move => h4 _ . case. by transitivity (Eps char) => //; symmetry. move => h4 _ _ . case. by transitivity (Void char) => //; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Atom uu s) => [ -> | [ -> | -> ]]. move => h3. case. by transitivity (Atom s) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Atom vv s) => [ -> | [ -> | -> ]]. move => h4. case. by transitivity (Atom s) => //; symmetry. move => h4 _ _ . case. by transitivity (Eps char) => //; symmetry. move => h4 _ . case. by transitivity (Void char) => //; symmetry. move => h3 _. case. by transitivity (Void char) => //; symmetry. * move => h1; apply cBar => [x]. case. case => [tt]. case : (wder_Atom tt s) => [ -> | [ -> | -> ]]. move => h2. + move => _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Atom uu s) => [ -> | [ -> | -> ]]. move => h3 _. case. by transitivity (Atom s) => //; symmetry. move => h3. case. by transitivity (Eps char) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Atom vv s) => [ -> | [ -> | -> ]]. move => h4 _. case. by transitivity (Atom s) => //; symmetry. move => h4 . case. by transitivity (Eps char) => //; symmetry. move => h4 _ _ . case. by transitivity (Void char) => //; symmetry. + move => h2. case. by transitivity (Eps char) => //; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Atom uu s) => [ -> | [ -> | -> ]]. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Atom vv s) => [ -> | [ -> | -> ]]. move => h4 _ _. case. by transitivity (Atom s) => //; symmetry. move => h4 . case. by transitivity (Eps char) => //; symmetry. move => h4 _ . case. by transitivity (Void char) => //; symmetry. move => h3. case. by transitivity (Eps char) => //; symmetry. move => h3 _. case. by transitivity (Void char) => //; symmetry. * move => h1; apply cBar => [x]. case. case => [tt]. case : (wder_Atom tt s) => [ -> | [ -> | -> ]]. move => h2. + move => _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Atom uu s) => [ -> | [ -> | -> ]]. move => h3 _. case. by transitivity (Atom s) => //; symmetry. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Atom vv s) => [ -> | [ -> | -> ]]. move => h4 _. case. by transitivity (Atom s) => //; symmetry. move => h4 _ _ . case. by transitivity (Eps char) => //; symmetry. move => h4 . case. by transitivity (Void char) => //; symmetry. move => h3. case. by transitivity (Void char) => //; symmetry. + move => h2 _. apply cBar => [x']. case => [] [[uu]]. case : (wder_Atom uu s) => [ -> | [ -> | -> ]]. move => h3 _ _. apply cBar => [z]. case => [] [[[vv]]]. case :(wder_Atom vv s) => [ -> | [ -> | -> ]]. move => h4 _ _. case. by transitivity (Atom s) => //; symmetry. move => h4 _ . case. by transitivity (Eps char) => //; symmetry. move => h4 . case. by transitivity (Void char) => //; symmetry. move => h3 _. case. by transitivity (Eps char) => //; symmetry. move => h3. case. by transitivity (Void char) => //; symmetry. + move => h2. case. by transitivity (Void char) => //; symmetry. - by apply: finite_der_Star. - by apply :finite_der_Plus. - by apply :finite_der_And. - by apply : finite_der_Conc. - by apply: finite_der_Not. Defined.
imports: Coq(RelationClasses Setoid Morphisms Permutation) Coq(SetoidList Mergesort Orders) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp)