proposition: Lemma deriv_mx_str_strict a: forall n (M: rmx n n), epsilon_mx M ≡ 0 -> deriv_mx a (M^*) ≡ deriv_mx a M ⋅ M^*.
proof: Proof. refine (mx_str_ind' (fun n M sM => epsilon_mx M ≡ 0 -> deriv_mx a sM ≡ deriv_mx a M ⋅ sM) _ _ _ _). intros n ? ? H ? ? H'. now rewrite H, H'. intros M _ i. elim (ord_0_empty i). intros M _ i j. setoid_rewrite ord0_unique. symmetry. apply cupxb. rename a into l. intros n m a b c d e be ec f fbe ecf He Hf HM. rewrite 2mx_map_blk, mx_dot_blk. unfold epsilon_mx in HM. rewrite mx_map_blk in HM. apply blk_mx_0 in HM as (Ha&Hb&Hc&Hd). assert (Hf': epsilon_mx (a+be⋅c) ≡ 0). rewrite epsilon_mx_pls, epsilon_mx_dot, Ha, Hc; ra. specialize (He Hd). specialize (Hf Hf'). unfold be in Hf. rewrite deriv_mx_pls, <-dotA, deriv_mx_dot, Hb, dot0x, cupxb in Hf. assert (Hecf: deriv_mx l ecf ≡ deriv_mx l c ⋅ f + deriv_mx l d ⋅ ecf). unfold ecf at 1, ec. rewrite <-dotA, deriv_mx_dot. rewrite He. unfold e at 2. rewrite epsilon_mx_str, Hd. rewrite deriv_mx_dot, Hc. unfold ecf, ec. ra. apply blk_mx_weq. - rewrite Hf. unfold ecf, ec. ra. - unfold fbe. rewrite deriv_mx_dot. unfold f at 2; rewrite epsilon_mx_str, Hf'. unfold be at 2. rewrite deriv_mx_dot. rewrite Hb. rewrite Hf. unfold ecf, be, ec. ra. - apply Hecf. - rewrite deriv_mx_pls, deriv_mx_dot, He, Hecf. unfold ecf at 2, ec. rewrite 2epsilon_mx_dot, Hc. unfold fbe. ra. Qed.
imports: monoid regex lset boolean sups matrix_ext normalisation