proposition: Lemma simpl_regex_language : forall A, mxF regex_language_f tt (MAUT.size (DFA.to_MAUT A)) (MAUT.size (DFA.to_MAUT A)) (MAUT.delta (DFA.to_MAUT A)) == box (DFA.size A) (DFA.size A) (fun s t => sum 0 (DFA.max_label A) (fun i => xif (eqb (state_of_nat t) (DFA.delta A (num_of_nat i) s)) (regex_language (RegExp.var (num_of_nat i))) 0)).
proof: Proof. intros A. Opaque regex_language_f. simpl. unfold labelling. Transparent regex_language_f. apply box_compat. intros s t. rewrite functor_sum. setoid_rewrite functor_xif. reflexivity. Qed.
imports: Coq(List) ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(Functors) ATBR(MxFunctors) ATBR(DKA_Definitions) ATBR(Model_Languages)