proposition: Lemma toolmkPlus3 : forall r1 r2, (r1 != CVoid /\ (forall l, r1 != CPlus l)) -> (r2 != CVoid /\ (forall l, r2 != CPlus l)) -> mkPlus r1 r2 = match compare r1 r2 with | Lt => CPlus [:: r1; r2] | Eq => r1 | Gt => CPlus [:: r2; r1] end .
proof: Proof. case => [ | | | s | c | l | l | l | c ] r2 [] //= _. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. - move => h. move/negP: (h l); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. - case : r2 => [ | | | t | d | k | k | k | d ] _ [] //= _. move => h. move/negP : (h k); by case. 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)