fact: Definition step (delta_set: label -> stateset -> stateset) loop p np := (fun a s => let q := delta_set a p in let '(table,d,next) := s in match StateSetMap.find q table with | None => loop (StateSetMap.add q next table, StateLabelMap.add (np,a) next d, S next) q next | Some nq => (table, StateLabelMap.add (np,a) nq d, next) end ).
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_StateSetSets) ATBR(Numbers) ATBR(Utils_WF)