YES 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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} DP: Strict: { 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)), plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(s(x), y) -> plus#(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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} EDG: {(quot#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y)) (plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(s(x), y) -> plus#(x, y)) (plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0())))) (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))) (plus#(s(x), y) -> plus#(x, y), plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0())))) (plus#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y)) (minus#(s(x), s(y)) -> minus#(x, y), minus#(s(x), s(y)) -> minus#(x, y))} SCCS: Scc: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(s(x), y) -> plus#(x, y)} Scc: {quot#(s(x), s(y)) -> quot#(minus(x, y), s(y))} Scc: {minus#(s(x), s(y)) -> minus#(x, y)} SCC: Strict: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(s(x), y) -> plus#(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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} POLY: Argument Filtering: pi(plus#) = [0,1], pi(plus) = [], pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0 Usable Rules: {} Interpretation: [plus#](x0, x1) = x0 + x1, [s](x0) = x0 + 1 Strict: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0())))} 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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} EDG: {(plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))))} SCCS: Scc: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0())))} SCC: Strict: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0())))} 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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} UR: { minus(x, 0()) -> x, minus(s(x), s(y)) -> minus(x, y)} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: {plus#_1(22, 25) -> 5* plus#_0(19, 17) -> 5* s_1(23) -> 24* s_1(20) -> 21* s_1(11) -> 20* s_0(19) -> 15* s_0(18) -> 18* s_0(17) -> 15* s_0(16) -> 18* s_0(15) -> 18* s_0(14) -> 16* s_0(11) -> 15* 0_1() -> 23* 0_0() -> 14* minus_1(11, 24) -> 25* minus_1(11, 23) -> 25* minus_1(11, 21) -> 22* minus_1(11, 20) -> 22* minus_1(11, 11) -> 22* minus_0(19, 19) -> 11* minus_0(19, 18) -> 19* minus_0(19, 17) -> 11* minus_0(19, 16) -> 17* minus_0(19, 15) -> 11* minus_0(19, 14) -> 11* minus_0(19, 11) -> 11* minus_0(18, 19) -> 11* minus_0(18, 18) -> 19* minus_0(18, 17) -> 11* minus_0(18, 16) -> 17* minus_0(18, 15) -> 11* minus_0(18, 14) -> 11* minus_0(18, 11) -> 11* minus_0(17, 19) -> 11* minus_0(17, 18) -> 19* minus_0(17, 17) -> 11* minus_0(17, 16) -> 17* minus_0(17, 15) -> 11* minus_0(17, 14) -> 11* minus_0(17, 11) -> 11* minus_0(16, 19) -> 11* minus_0(16, 18) -> 19* minus_0(16, 17) -> 11* minus_0(16, 16) -> 17* minus_0(16, 15) -> 11* minus_0(16, 14) -> 11* minus_0(16, 11) -> 11* minus_0(15, 19) -> 11* minus_0(15, 18) -> 19* minus_0(15, 17) -> 11* minus_0(15, 16) -> 17* minus_0(15, 15) -> 11* minus_0(15, 14) -> 11* minus_0(15, 11) -> 11* minus_0(14, 19) -> 11* minus_0(14, 18) -> 19* minus_0(14, 17) -> 11* minus_0(14, 16) -> 17* minus_0(14, 15) -> 11* minus_0(14, 14) -> 11* minus_0(14, 11) -> 11* minus_0(11, 19) -> 11* minus_0(11, 18) -> 19* minus_0(11, 17) -> 11* minus_0(11, 16) -> 19 | 17 minus_0(11, 15) -> 19 | 11 minus_0(11, 14) -> 17 | 11 minus_0(11, 11) -> 19 | 11 19 -> 11* 18 -> 11* 17 -> 11* 16 -> 11* 15 -> 11* 14 -> 11* 11 -> 25 | 22 | 19 | 17} Strict: {} Qed SCC: 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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} POLY: Argument Filtering: pi(plus) = [], pi(quot#) = [0,1], pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0 Usable Rules: {} Interpretation: [quot#](x0, x1) = x0 + x1, [s](x0) = x0 + 1 Strict: {} 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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} Qed SCC: 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))), plus(minus(x, s(0())), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0()))), plus(0(), y) -> y, plus(s(x), y) -> s(plus(x, y))} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed