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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} 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), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} 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)) -> quot#(minus(x, y), s(y))) (quot#(s(x), s(y)) -> quot#(minus(x, y), s(y)), quot#(s(x), s(y)) -> minus#(x, y)) (plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0()))), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0())))) (plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0()))), plus#(s(x), y) -> plus#(x, y)) (plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0()))), 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()))), 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()))), 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#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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#(s(x), y) -> plus#(x, y), plus#(s(x), y) -> plus#(x, y)) (plus#(s(x), y) -> plus#(x, y), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0())))) (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), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0())))} 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), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} POLY: Argument Filtering: pi(plus#) = [0,1], pi(plus) = [0,1], pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0 Usable Rules: {} Interpretation: [plus#](x0, x1) = x0 + x1, [plus](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [0] = 1 Strict: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0()))), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} EDG: {(plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0()))), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0())))) (plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(x, s(0()))), 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()))), 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()))), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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()))), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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()))), plus#(plus(x, s(0())), plus(y, s(s(z)))) -> plus#(plus(y, s(s(z))), plus(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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} UR: { minus(x, 0()) -> x, 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(0(), y) -> y, plus(s(x), y) -> s(plus(x, y)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: {plus#_0(21, 18) -> 6* plus_0(21, 21) -> 13* plus_0(21, 20) -> 21* plus_0(21, 19) -> 18* plus_0(21, 18) -> 13* plus_0(21, 17) -> 13* plus_0(21, 16) -> 13* plus_0(21, 13) -> 13* plus_0(21, 12) -> 13* plus_0(20, 21) -> 13* plus_0(20, 20) -> 21* plus_0(20, 19) -> 18* plus_0(20, 18) -> 13* plus_0(20, 17) -> 13* plus_0(20, 16) -> 13* plus_0(20, 13) -> 13* plus_0(20, 12) -> 13* plus_0(19, 21) -> 13* plus_0(19, 20) -> 21* plus_0(19, 19) -> 18* plus_0(19, 18) -> 13* plus_0(19, 17) -> 13* plus_0(19, 16) -> 13* plus_0(19, 13) -> 13* plus_0(19, 12) -> 13* plus_0(18, 21) -> 13* plus_0(18, 20) -> 21* plus_0(18, 19) -> 18* plus_0(18, 18) -> 13* plus_0(18, 17) -> 13* plus_0(18, 16) -> 13* plus_0(18, 13) -> 13* plus_0(18, 12) -> 13* plus_0(17, 21) -> 13* plus_0(17, 20) -> 21* plus_0(17, 19) -> 18* plus_0(17, 18) -> 13* plus_0(17, 17) -> 13* plus_0(17, 16) -> 13* plus_0(17, 13) -> 13* plus_0(17, 12) -> 13* plus_0(16, 21) -> 13* plus_0(16, 20) -> 21* plus_0(16, 19) -> 18* plus_0(16, 18) -> 13* plus_0(16, 17) -> 13* plus_0(16, 16) -> 13* plus_0(16, 13) -> 13* plus_0(16, 12) -> 13* plus_0(13, 21) -> 13* plus_0(13, 20) -> 21* plus_0(13, 19) -> 18* plus_0(13, 18) -> 13* plus_0(13, 17) -> 13* plus_0(13, 16) -> 13* plus_0(13, 13) -> 13* plus_0(13, 12) -> 13* plus_0(12, 21) -> 13* plus_0(12, 20) -> 21* plus_0(12, 19) -> 18* plus_0(12, 18) -> 13* plus_0(12, 17) -> 13* plus_0(12, 16) -> 13* plus_0(12, 13) -> 13* plus_0(12, 12) -> 13* s_0(21) -> 17* s_0(20) -> 20* s_0(19) -> 20* s_0(18) -> 17* s_0(17) -> 20* s_0(16) -> 19* s_0(13) -> 21 | 18 | 17 s_0(12) -> 17* 0_0() -> 16* minus_0(21, 21) -> 12* minus_0(21, 20) -> 12* minus_0(21, 19) -> 12* minus_0(21, 18) -> 12* minus_0(21, 17) -> 12* minus_0(21, 16) -> 12* minus_0(21, 13) -> 12* minus_0(21, 12) -> 12* minus_0(20, 21) -> 12* minus_0(20, 20) -> 12* minus_0(20, 19) -> 12* minus_0(20, 18) -> 12* minus_0(20, 17) -> 12* minus_0(20, 16) -> 12* minus_0(20, 13) -> 12* minus_0(20, 12) -> 12* minus_0(19, 21) -> 12* minus_0(19, 20) -> 12* minus_0(19, 19) -> 12* minus_0(19, 18) -> 12* minus_0(19, 17) -> 12* minus_0(19, 16) -> 12* minus_0(19, 13) -> 12* minus_0(19, 12) -> 12* minus_0(18, 21) -> 12* minus_0(18, 20) -> 12* minus_0(18, 19) -> 12* minus_0(18, 18) -> 12* minus_0(18, 17) -> 12* minus_0(18, 16) -> 12* minus_0(18, 13) -> 12* minus_0(18, 12) -> 12* minus_0(17, 21) -> 12* minus_0(17, 20) -> 12* minus_0(17, 19) -> 12* minus_0(17, 18) -> 12* minus_0(17, 17) -> 12* minus_0(17, 16) -> 12* minus_0(17, 13) -> 12* minus_0(17, 12) -> 12* minus_0(16, 21) -> 12* minus_0(16, 20) -> 12* minus_0(16, 19) -> 12* minus_0(16, 18) -> 12* minus_0(16, 17) -> 12* minus_0(16, 16) -> 12* minus_0(16, 13) -> 12* minus_0(16, 12) -> 12* minus_0(13, 21) -> 12* minus_0(13, 20) -> 12* minus_0(13, 19) -> 12* minus_0(13, 18) -> 12* minus_0(13, 17) -> 12* minus_0(13, 16) -> 12* minus_0(13, 13) -> 12* minus_0(13, 12) -> 12* minus_0(12, 21) -> 12* minus_0(12, 20) -> 12* minus_0(12, 19) -> 12* minus_0(12, 18) -> 12* minus_0(12, 17) -> 12* minus_0(12, 16) -> 12* minus_0(12, 13) -> 12* minus_0(12, 12) -> 12* 21 -> 12* 20 -> 21 | 12 19 -> 18 | 12 18 -> 12* 17 -> 12* 16 -> 12* 13 -> 12* 12 -> 13*} Strict: {plus#(minus(x, s(0())), minus(y, s(s(z)))) -> plus#(minus(y, s(s(z))), minus(x, s(0())))} 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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} 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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} POLY: Argument Filtering: pi(plus) = [], pi(quot#) = 0, pi(quot) = [], pi(s) = [0], pi(0) = [], pi(minus) = 0 Usable Rules: {} Interpretation: [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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} 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)), plus(plus(x, s(0())), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0())))} SPSC: Simple Projection: pi(minus#) = 0 Strict: {} Qed