fact: Fixpoint loop n (w: list label) tarjan (x y: state) : DS.UF + bool * list num := match n with | Datatypes.S n => let '(b,tarjan) := DS.test_and_unify tarjan x y in if b then inl tarjan else let fx := final x in let fy := final y in if eq_bool_bool fx fy then fold_num_sum (fun a tarjan => loop n (a::w) tarjan (d a x) (d a y)) m tarjan else inr (fx, rev w) | O => inl tarjan 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(Utils_WF) Coq(Relations) Coq(List)