MAYBE Time: 0.000953 TRS: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y)} DP: DP: {minus#(s 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: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y)} EDG: {(quot#(s x, s y) -> minus#(x, y), minus#(s 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)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y))} STATUS: arrows: 0.555556 SCCS (2): Scc: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Scc: {minus#(s x, s y) -> minus#(x, y)} SCC (1): Strict: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y)} Open SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { minus(x, 0()) -> x, minus(s x, s y) -> minus(x, y), quot(0(), s y) -> 0(), quot(s x, s y) -> s quot(minus(x, y), s y)} Open