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