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