MAYBE Time: 0.075330 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: DP: { 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()))} 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()))} 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())), a(w, v) -> w, a(w, v) -> v} 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))} STATUS: arrows: 0.638889 SCCS (3): Scc: {quot#(s x, s y) -> quot#(minus(x, y), s y)} 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: {minus#(s x, s y) -> minus#(x, y)} SCC (1): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0, [quot](x0, x1) = x0 + 1, [plus](x0, x1) = 0, [s](x0) = x0 + 1, [0] = 1, [quot#](x0, x1) = x0 + 1 Strict: quot#(s x, s y) -> quot#(minus(x, y), s y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0())) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z plus(s x, y) -> s plus(x, y) 0 + 0x + 0y >= 1 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y plus(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 1y >= 3 + 0x + 1y quot(0(), s y) -> 0() 2 + 1y >= 1 minus(s x, s y) -> minus(x, y) 1 + 1x + 0y >= 0 + 1x + 0y minus(x, 0()) -> x 0 + 1x >= 1x Qed SCC (3): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0, [quot](x0, x1) = x0, [plus](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [0] = 1, [plus#](x0, x1) = x0 + x1 Strict: plus#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())) 4 + 1x + 1y + 1z >= 4 + 1x + 1y + 1z plus#(s x, y) -> plus#(x, y) 1 + 1x + 1y >= 0 + 1x + 1y plus#(minus(x, s 0()), minus(y, s s z)) -> plus#(minus(y, s s z), minus(x, s 0())) 0 + 1x + 1y + 0z >= 0 + 1x + 1y + 0z Weak: plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0())) 4 + 1x + 1y + 1z >= 4 + 1x + 1y + 1z plus(s x, y) -> s plus(x, y) 1 + 1x + 1y >= 1 + 1x + 1y plus(0(), y) -> y 1 + 1y >= 1y plus(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())) 0 + 1x + 1y + 0z >= 0 + 1x + 1y + 0z quot(s x, s y) -> s quot(minus(x, y), s y) 1 + 1x + 0y >= 1 + 1x + 0y quot(0(), s y) -> 0() 1 + 0y >= 1 minus(s x, s y) -> minus(x, y) 1 + 1x + 0y >= 0 + 1x + 0y minus(x, 0()) -> x 0 + 1x >= 1x SCCS (1): 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 (2): 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()))} Fail SCC (1): 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()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [plus](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [minus#](x0, x1) = x0 Strict: minus#(s x, s y) -> minus#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: plus(plus(x, s 0()), plus(y, s s z)) -> plus(plus(y, s s z), plus(x, s 0())) 2 + 1x + 0y + 0z >= 2 + 0x + 1y + 0z plus(s x, y) -> s plus(x, y) 2 + 1x + 0y >= 2 + 1x + 0y plus(0(), y) -> y 2 + 0y >= 1y plus(minus(x, s 0()), minus(y, s s z)) -> plus(minus(y, s s z), minus(x, s 0())) 4 + 0x + 0y + 0z >= 4 + 0x + 0y + 1z quot(s x, s y) -> s quot(minus(x, y), s y) 2 + 0x + 1y >= 3 + 0x + 1y quot(0(), s y) -> 0() 2 + 1y >= 1 minus(s x, s y) -> minus(x, y) 2 + 0x + 1y >= 1 + 0x + 1y minus(x, 0()) -> x 2 + 0x >= 1x Qed