proposition: Theorem construction_correct: forall (e: regex), MAUT.eval (X_to_MAUT e) == e.
proof: Proof. intro e. eapply equal_trans. apply build_correct; auto with arith. Transparent dot star plus one zero Peano.minus. compute; fold_regex. kleene_clean_zeros. semiring_reflexivity. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(DKA_CheckLabels) ATBR(StrictStarForm) ATBR(Utils_WF) Coq(Relations)