proposition: Lemma wf_CAnd_nand_nand : forall r1 r2, wf_re r1 -> wf_re r2 -> [/\ r1 != CVoid , r1 != CNot CVoid & (forall l, r1 != CAnd l)] -> [/\ r2 != CVoid , r2 != CNot CVoid & (forall l, r2 != CAnd l)] -> wf_re (mkAnd r1 r2).
proof: Proof. move => r1 r2 hw1 hw2 hh1 hh2. rewrite toolmkAnd3 /mkAnd => //. case_eq (compare r1 r2) => heq //=. - apply/andP; split. rewrite andbT. apply/negP. rewrite mem_seq1 => heq2. by rewrite (eqP heq2) compare_refl in heq. apply/andP; split. rewrite andbT. by rewrite /cregexp_le /leS /cmpS /= heq. by rewrite hw1 hw2. - apply/andP; split. rewrite andbT. apply/negP. rewrite mem_seq1 => heq2. by rewrite (eqP heq2) compare_refl in heq. apply/andP; split. rewrite andbT. move : heq. rewrite compare_neg /cregexp_le /leS /cmpS /=. case: (compare r2 r1) => //=. by rewrite hw1 hw2. 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)