MAYBE Time: 0.064408 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()))} 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))} SCCS (3): 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: {quot#(s x, s y) -> quot#(minus(x, y), s y)} Scc: {minus#(s x, s y) -> minus#(x, y)} 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: EDG: {(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#(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#(plus(x, s 0()), plus(y, s s z)) -> plus#(plus(y, s s z), plus(x, s 0())))} 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: {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: Qed 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()))} SPSC: Simple Projection: pi(minus#) = 1 Strict: {} Qed