proposition: Lemma mkAndAC: forall r1 r2 r3, wf_re r1 -> wf_re r2 -> wf_re r3 -> mkAnd (mkAnd r1 r2) r3 = mkAnd (mkAnd r1 r3) r2.
proof: Proof. move => r1 r2 r3. case: (toolmkAnd r1). - move => heq; rewrite (eqP heq); clear heq r1. by rewrite !mkAnd_CVoid_lt. - move => heq; rewrite (eqP heq); clear heq r1. by rewrite !mkAnd_CAll_lt mkAndC. - case => l1 heq; rewrite (eqP heq); clear heq r1. move => hw1. case: (toolmkAnd r2). + move => heq; rewrite (eqP heq); clear heq r2. by rewrite !mkAnd_CVoid_rt. + move => heq; rewrite (eqP heq); clear heq r2. by rewrite !mkAnd_CAll_rt. + case => l2 heq; rewrite (eqP heq); clear heq r2. move => hw2. case : (toolmkAnd r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CVoid_rt. * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CAll_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. by rewrite mkAndAC_and_and_and. * move => hh1 hw3. by rewrite mkAndAC_and_and_nand. + move => hh1 hw2. case: (toolmkAnd r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CVoid_rt. * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CAll_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. by rewrite mkAndAC_and_and_nand. * move => hh3 hw3. rewrite !(mkAndC (CAnd l1) _ ). rewrite -!mkAndAC_nand_nand_and => //. by rewrite (mkAndC r2 r3). - move => hh1 hw1. case: (toolmkAnd r2). + move => heq; rewrite (eqP heq); clear heq r2. by rewrite !mkAnd_CVoid_rt. + move => heq; rewrite (eqP heq); clear heq r2. by rewrite !mkAnd_CAll_rt. + case => l2 heq; rewrite (eqP heq) => hw2; clear heq r2. case : (toolmkAnd r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CVoid_rt. * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CAll_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. rewrite !(mkAndC r1). rewrite -!mkAndAC_and_and_nand => //. by rewrite (mkAndC (CAnd l2) (CAnd l3)). * move => hh2 hw3. by rewrite mkAndAC_nand_nand_and. + move => hh2 hw2. case: (toolmkAnd r3). * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CVoid_rt. * move => heq; rewrite (eqP heq); clear heq r3. by rewrite !mkAnd_CAll_rt. * case => l3 heq ; rewrite (eqP heq) => hw3 ; clear heq r3. by rewrite mkAndAC_nand_nand_and. * move => hh3 w3. by rewrite mkAndAC_nand_nand_nand. 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)