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