YES 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: Strict: { 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))} 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()} EDG: {(quot#(s(x), s(y)) -> minus#(x, y), minus#(x, s(y)) -> minus#(x, y)) (quot#(s(x), s(y)) -> minus#(x, y), minus#(x, s(y)) -> pred#(minus(x, y))) (minus#(x, s(y)) -> minus#(x, y), minus#(x, s(y)) -> pred#(minus(x, y))) (minus#(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)))} SCCS: Scc: {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))} Scc: {minus#(x, s(y)) -> minus#(x, y)} SCC: 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()} POLY: Argument Filtering: pi(quot#) = 0, pi(quot) = [], pi(0) = [], pi(minus) = 0, pi(s) = [0], pi(pred) = 0 Usable Rules: {} Interpretation: [s](x0) = x0 + 1 Strict: {} 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()} Qed SCC: 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()} SPSC: Simple Projection: pi(minus#) = 1 Strict: {} Qed