fact: Definition preNFA_to_preMAUT (A: pre_eNFA): Algebraic.pre_MAUT := let n := nat_of_state (size A) in Algebraic.mk (mx_bool _ n n (fun i j => epsilonbrel A (state_of_nat i) (state_of_nat j)) + box n n (fun i j => labelling (max_label A) (fun a => deltabrel A (state_of_nat i) a (state_of_nat j)))).
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)