fact: Definition to_MAUT A := let n := nat_of_state (size A) in MAUT.mk (mx_point 1 n 0 (initial A) 1) (box n n (fun i j => labelling (max_label A) (fun a => eq_state_bool (state_of_nat j) (delta A a i)))) (mx_bool _ n 1 (fun i _ => StateSet.mem i (finaux A))).
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)