YES Time: 0.031761 TRS: {plus(x, s s y) -> s plus(s x, y), plus(s s x, y) -> s plus(x, s y), plus(s 0(), y) -> s y, plus(0(), y) -> y, ack(s x, s y) -> ack(x, plus(y, ack(s x, y))), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} DP: DP: {plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y), ack#(s x, s y) -> plus#(y, ack(s x, y)), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())} TRS: {plus(x, s s y) -> s plus(s x, y), plus(s s x, y) -> s plus(x, s y), plus(s 0(), y) -> s y, plus(0(), y) -> y, ack(s x, s y) -> ack(x, plus(y, ack(s x, y))), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} UR: {plus(x, s s y) -> s plus(s x, y), plus(s s x, y) -> s plus(x, s y), plus(s 0(), y) -> s y, plus(0(), y) -> y, ack(s x, s y) -> ack(x, plus(y, ack(s x, y))), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y, a(z, w) -> z, a(z, w) -> w} EDG: {(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> plus#(y, ack(s x, y))) (plus#(x, s s y) -> plus#(s x, y), plus#(x, s s y) -> plus#(s x, y)) (plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y)) (plus#(s s x, y) -> plus#(x, s y), plus#(x, s s y) -> plus#(s x, y)) (plus#(s s x, y) -> plus#(x, s y), plus#(s s x, y) -> plus#(x, s y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(x, s s y) -> plus#(s x, y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(s s x, y) -> plus#(x, s y))} EDG: {(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> plus#(y, ack(s x, y))) (plus#(x, s s y) -> plus#(s x, y), plus#(x, s s y) -> plus#(s x, y)) (plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y)) (plus#(s s x, y) -> plus#(x, s y), plus#(x, s s y) -> plus#(s x, y)) (plus#(s s x, y) -> plus#(x, s y), plus#(s s x, y) -> plus#(x, s y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(x, s s y) -> plus#(s x, y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(s s x, y) -> plus#(x, s y))} EDG: {(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> plus#(y, ack(s x, y))) (plus#(x, s s y) -> plus#(s x, y), plus#(x, s s y) -> plus#(s x, y)) (plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y)) (plus#(s s x, y) -> plus#(x, s y), plus#(x, s s y) -> plus#(s x, y)) (plus#(s s x, y) -> plus#(x, s y), plus#(s s x, y) -> plus#(x, s y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(x, s s y) -> plus#(s x, y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(s s x, y) -> plus#(x, s y))} EDG: {(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> plus#(y, ack(s x, y))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y)))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> plus#(y, ack(s x, y))) (plus#(x, s s y) -> plus#(s x, y), plus#(x, s s y) -> plus#(s x, y)) (plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y)) (plus#(s s x, y) -> plus#(x, s y), plus#(x, s s y) -> plus#(s x, y)) (plus#(s s x, y) -> plus#(x, s y), plus#(s s x, y) -> plus#(x, s y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(x, s s y) -> plus#(s x, y)) (ack#(s x, s y) -> plus#(y, ack(s x, y)), plus#(s s x, y) -> plus#(x, s y))} STATUS: arrows: 0.555556 SCCS (2): Scc: {ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())} Scc: {plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y)} SCC (3): Strict: {ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))), ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())} Weak: {plus(x, s s y) -> s plus(s x, y), plus(s s x, y) -> s plus(x, s y), plus(s 0(), y) -> s y, plus(0(), y) -> y, ack(s x, s y) -> ack(x, plus(y, ack(s x, y))), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + 1, [ack](x0, x1) = 0, [s](x0) = x0 + 1, [0] = 1, [ack#](x0, x1) = x0 Strict: ack#(s x, 0()) -> ack#(x, s 0()) 1 + 1x >= 0 + 1x ack#(s x, s y) -> ack#(s x, y) 1 + 1x + 0y >= 1 + 1x + 0y ack#(s x, s y) -> ack#(x, plus(y, ack(s x, y))) 1 + 1x + 0y >= 0 + 1x + 0y Weak: ack(0(), y) -> s y 0 + 0y >= 1 + 1y ack(s x, 0()) -> ack(x, s 0()) 0 + 0x >= 0 + 0x ack(s x, s y) -> ack(x, plus(y, ack(s x, y))) 0 + 0x + 0y >= 0 + 0x + 0y plus(0(), y) -> y 2 + 0y >= 1y plus(s 0(), y) -> s y 3 + 0y >= 1 + 1y plus(s s x, y) -> s plus(x, s y) 3 + 1x + 0y >= 2 + 1x + 0y plus(x, s s y) -> s plus(s x, y) 1 + 1x + 0y >= 3 + 1x + 0y SCCS (1): Scc: {ack#(s x, s y) -> ack#(s x, y)} SCC (1): Strict: {ack#(s x, s y) -> ack#(s x, y)} Weak: {plus(x, s s y) -> s plus(s x, y), plus(s s x, y) -> s plus(x, s y), plus(s 0(), y) -> s y, plus(0(), y) -> y, ack(s x, s y) -> ack(x, plus(y, ack(s x, y))), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = x0 + 1, [ack](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 0, [ack#](x0, x1) = x0 + x1 Strict: ack#(s x, s y) -> ack#(s x, y) 2 + 1x + 1y >= 1 + 1x + 1y Weak: ack(0(), y) -> s y 1 + 0y >= 1 + 1y ack(s x, 0()) -> ack(x, s 0()) 2 + 1x >= 1 + 1x ack(s x, s y) -> ack(x, plus(y, ack(s x, y))) 2 + 1x + 0y >= 1 + 1x + 0y plus(0(), y) -> y 1 + 0y >= 1y plus(s 0(), y) -> s y 2 + 0y >= 1 + 1y plus(s s x, y) -> s plus(x, s y) 3 + 1x + 0y >= 2 + 1x + 0y plus(x, s s y) -> s plus(s x, y) 1 + 1x + 0y >= 3 + 1x + 0y Qed SCC (2): Strict: {plus#(x, s s y) -> plus#(s x, y), plus#(s s x, y) -> plus#(x, s y)} Weak: {plus(x, s s y) -> s plus(s x, y), plus(s s x, y) -> s plus(x, s y), plus(s 0(), y) -> s y, plus(0(), y) -> y, ack(s x, s y) -> ack(x, plus(y, ack(s x, y))), ack(s x, 0()) -> ack(x, s 0()), ack(0(), y) -> s y} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [plus](x0, x1) = 0, [ack](x0, x1) = 0, [s](x0) = x0 + 1, [0] = 1, [plus#](x0, x1) = x0 + x1 + 1 Strict: plus#(s s x, y) -> plus#(x, s y) 3 + 1x + 1y >= 2 + 1x + 1y plus#(x, s s y) -> plus#(s x, y) 3 + 1x + 1y >= 2 + 1x + 1y Weak: ack(0(), y) -> s y 0 + 0y >= 1 + 1y ack(s x, 0()) -> ack(x, s 0()) 0 + 0x >= 0 + 0x ack(s x, s y) -> ack(x, plus(y, ack(s x, y))) 0 + 0x + 0y >= 0 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y plus(s 0(), y) -> s y 0 + 0y >= 1 + 1y plus(s s x, y) -> s plus(x, s y) 0 + 0x + 0y >= 1 + 0x + 0y plus(x, s s y) -> s plus(s x, y) 0 + 0x + 0y >= 1 + 0x + 0y Qed