MAYBE Time: 0.001059 TRS: { pred s x -> x, minus(x, s y) -> pred minus(x, y), minus(x, 0()) -> x, quot(s x, s y) -> s quot(minus(x, y), s y), quot(0(), s y) -> 0()} DP: DP: { minus#(x, s y) -> pred# minus(x, y), minus#(x, s y) -> minus#(x, y), quot#(s x, s y) -> minus#(x, y), quot#(s x, s y) -> quot#(minus(x, y), s y)} TRS: { pred s x -> x, minus(x, s y) -> pred minus(x, y), minus(x, 0()) -> x, quot(s x, s y) -> s quot(minus(x, y), s y), quot(0(), s y) -> 0()} EDG: {(minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y)) (minus#(x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y)) (quot#(s x, s y) -> minus#(x, y), minus#(x, s y) -> pred# minus(x, y)) (quot#(s x, s y) -> minus#(x, y), minus#(x, s y) -> minus#(x, y)) (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> minus#(x, y)) (quot#(s x, s y) -> quot#(minus(x, y), s y), quot#(s x, s y) -> quot#(minus(x, y), s y))} STATUS: arrows: 0.625000 SCCS (2): Scc: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Scc: {minus#(x, s y) -> minus#(x, y)} SCC (1): Strict: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Weak: { pred s x -> x, minus(x, s y) -> pred minus(x, y), minus(x, 0()) -> x, quot(s x, s y) -> s quot(minus(x, y), s y), quot(0(), s y) -> 0()} Open SCC (1): Strict: {minus#(x, s y) -> minus#(x, y)} Weak: { pred s x -> x, minus(x, s y) -> pred minus(x, y), minus(x, 0()) -> x, quot(s x, s y) -> s quot(minus(x, y), s y), quot(0(), s y) -> 0()} Open