fact: Definition to_MAUT A := let n := nat_of_state (size A) in MAUT.mk (mx_point 1 n 0 (initial A) 1) (mx_bool _ n n (fun i j => StateSet.mem j (epsilon A i)) + box n n (fun i j => labelling (max_label A) (fun a => StateSet.mem j (delta A a i)))) (mx_point n 1 (final A) 0 1).
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(MyFSets) ATBR(MyFSetProperties) ATBR(MyFMapProperties)