MAYBE Time: 1.053933 TRS: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} DP: DP: { permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(x, y, a()) -> isZero# x, permute#(y, x, c()) -> permute#(x, y, a()), permute#(false(), x, b()) -> permute#(ack(x, x), p x, c()), permute#(false(), x, b()) -> ack#(x, x), permute#(false(), x, b()) -> p# x, double# x -> permute#(x, x, a()), ack#(0(), x) -> plus#(x, s 0()), ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y), plus#(x, s s y) -> plus#(s x, y), plus#(s x, y) -> plus#(x, s y)} TRS: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} UR: { isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y), d(z, w) -> z, d(z, w) -> w} EDG: {(ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(s x, y)) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, 0()) -> ack#(x, s 0()), ack#(0(), x) -> plus#(x, s 0())) (permute#(y, x, c()) -> permute#(x, y, a()), permute#(x, y, a()) -> isZero# x) (permute#(y, x, c()) -> permute#(x, y, a()), permute#(x, y, a()) -> permute#(isZero x, x, b())) (double# x -> permute#(x, x, a()), permute#(x, y, a()) -> isZero# x) (double# x -> permute#(x, x, a()), permute#(x, y, a()) -> permute#(isZero x, x, b())) (plus#(x, s s y) -> plus#(s x, y), plus#(s x, y) -> plus#(x, s y)) (plus#(x, s s y) -> plus#(s x, y), plus#(x, s s y) -> plus#(s x, y)) (permute#(false(), x, b()) -> ack#(x, x), ack#(s x, s y) -> ack#(s x, y)) (permute#(false(), x, b()) -> ack#(x, x), ack#(s x, s y) -> ack#(x, ack(s x, y))) (permute#(false(), x, b()) -> ack#(x, x), ack#(s x, 0()) -> ack#(x, s 0())) (permute#(false(), x, b()) -> ack#(x, x), ack#(0(), x) -> plus#(x, s 0())) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(0(), x) -> plus#(x, s 0())) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y)) (plus#(s x, y) -> plus#(x, s y), plus#(x, s s y) -> plus#(s x, y)) (plus#(s x, y) -> plus#(x, s y), plus#(s x, y) -> plus#(x, s y)) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, 0()) -> ack#(x, s 0())) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(x, ack(s x, y))) (ack#(s x, s y) -> ack#(s x, y), ack#(s x, s y) -> ack#(s x, y)) (permute#(false(), x, b()) -> permute#(ack(x, x), p x, c()), permute#(y, x, c()) -> permute#(x, y, a())) (permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(false(), x, b()) -> permute#(ack(x, x), p x, c())) (permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(false(), x, b()) -> ack#(x, x)) (permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(false(), x, b()) -> p# x) (ack#(0(), x) -> plus#(x, s 0()), plus#(s x, y) -> plus#(x, s y))} STATUS: arrows: 0.840237 SCCS (3): Scc: { permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(y, x, c()) -> permute#(x, y, a()), permute#(false(), x, b()) -> permute#(ack(x, x), p x, c())} Scc: {ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y)} Scc: {plus#(x, s s y) -> plus#(s x, y), plus#(s x, y) -> plus#(x, s y)} SCC (3): Strict: { permute#(x, y, a()) -> permute#(isZero x, x, b()), permute#(y, x, c()) -> permute#(x, y, a()), permute#(false(), x, b()) -> permute#(ack(x, x), p x, c())} Weak: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} Fail SCC (3): Strict: {ack#(s x, 0()) -> ack#(x, s 0()), ack#(s x, s y) -> ack#(x, ack(s x, y)), ack#(s x, s y) -> ack#(s x, y)} Weak: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [permute](x0, x1, x2) = x0 + x1, [ack](x0, x1) = 0, [plus](x0, x1) = 0, [double](x0) = 0, [isZero](x0) = x0, [p](x0) = 0, [s](x0) = x0 + 1, [a] = 0, [b] = 0, [c] = 0, [false] = 0, [0] = 0, [true] = 0, [ack#](x0, x1) = x0 Strict: ack#(s x, s y) -> ack#(s x, y) 1 + 1x + 0y >= 1 + 1x + 0y ack#(s x, s y) -> ack#(x, ack(s x, y)) 1 + 1x + 0y >= 0 + 1x + 0y ack#(s x, 0()) -> ack#(x, s 0()) 1 + 1x >= 0 + 1x Weak: plus(s x, y) -> plus(x, s y) 0 + 0x + 0y >= 0 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y plus(x, s s y) -> s plus(s x, y) 0 + 0x + 0y >= 1 + 0x + 0y plus(x, s 0()) -> s x 0 + 0x >= 1 + 1x plus(x, 0()) -> x 0 + 0x >= 1x p s x -> x 0 + 0x >= 1x p 0() -> 0() 0 >= 0 ack(s x, s y) -> ack(x, ack(s x, y)) 0 + 0x + 0y >= 0 + 0x + 0y ack(s x, 0()) -> ack(x, s 0()) 0 + 0x >= 0 + 0x ack(0(), x) -> plus(x, s 0()) 0 + 0x >= 0 + 0x isZero s x -> false() 1 + 1x >= 0 isZero 0() -> true() 0 >= 0 double x -> permute(x, x, a()) 0 + 0x >= 0 + 2x permute(true(), x, b()) -> 0() 0 + 1x >= 0 permute(false(), x, b()) -> permute(ack(x, x), p x, c()) 0 + 1x >= 0 + 0x permute(y, x, c()) -> s s permute(x, y, a()) 0 + 1x + 1y >= 2 + 1x + 1y permute(x, y, a()) -> permute(isZero x, x, b()) 0 + 1x + 1y >= 0 + 2x SCCS (1): Scc: {ack#(s x, s y) -> ack#(s x, y)} SCC (1): Strict: {ack#(s x, s y) -> ack#(s x, y)} Weak: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [permute](x0, x1, x2) = x0 + x1, [ack](x0, x1) = 1, [plus](x0, x1) = 0, [double](x0) = 0, [isZero](x0) = x0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [a] = 0, [b] = 0, [c] = 0, [false] = 0, [0] = 0, [true] = 0, [ack#](x0, x1) = x0 + 1 Strict: ack#(s x, s y) -> ack#(s x, y) 2 + 0x + 1y >= 1 + 0x + 1y Weak: plus(s x, y) -> plus(x, s y) 0 + 0x + 0y >= 0 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y plus(x, s s y) -> s plus(s x, y) 0 + 0x + 0y >= 1 + 0x + 0y plus(x, s 0()) -> s x 0 + 0x >= 1 + 1x plus(x, 0()) -> x 0 + 0x >= 1x p s x -> x 2 + 1x >= 1x p 0() -> 0() 1 >= 0 ack(s x, s y) -> ack(x, ack(s x, y)) 1 + 0x + 0y >= 1 + 0x + 0y ack(s x, 0()) -> ack(x, s 0()) 1 + 0x >= 1 + 0x ack(0(), x) -> plus(x, s 0()) 1 + 0x >= 0 + 0x isZero s x -> false() 1 + 1x >= 0 isZero 0() -> true() 0 >= 0 double x -> permute(x, x, a()) 0 + 0x >= 0 + 2x permute(true(), x, b()) -> 0() 0 + 1x >= 0 permute(false(), x, b()) -> permute(ack(x, x), p x, c()) 0 + 1x >= 2 + 1x permute(y, x, c()) -> s s permute(x, y, a()) 0 + 1x + 1y >= 2 + 1x + 1y permute(x, y, a()) -> permute(isZero x, x, b()) 0 + 1x + 1y >= 0 + 2x Qed SCC (2): Strict: {plus#(x, s s y) -> plus#(s x, y), plus#(s x, y) -> plus#(x, s y)} Weak: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [permute](x0, x1, x2) = x0 + x1, [ack](x0, x1) = 1, [plus](x0, x1) = 0, [double](x0) = 0, [isZero](x0) = x0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [a] = 0, [b] = 0, [c] = 0, [false] = 0, [0] = 0, [true] = 0, [plus#](x0, x1) = x0 + x1 Strict: plus#(s x, y) -> plus#(x, s y) 1 + 1x + 1y >= 1 + 1x + 1y plus#(x, s s y) -> plus#(s x, y) 2 + 1x + 1y >= 1 + 1x + 1y Weak: plus(s x, y) -> plus(x, s y) 0 + 0x + 0y >= 0 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y plus(x, s s y) -> s plus(s x, y) 0 + 0x + 0y >= 1 + 0x + 0y plus(x, s 0()) -> s x 0 + 0x >= 1 + 1x plus(x, 0()) -> x 0 + 0x >= 1x p s x -> x 2 + 1x >= 1x p 0() -> 0() 1 >= 0 ack(s x, s y) -> ack(x, ack(s x, y)) 1 + 0x + 0y >= 1 + 0x + 0y ack(s x, 0()) -> ack(x, s 0()) 1 + 0x >= 1 + 0x ack(0(), x) -> plus(x, s 0()) 1 + 0x >= 0 + 0x isZero s x -> false() 1 + 1x >= 0 isZero 0() -> true() 0 >= 0 double x -> permute(x, x, a()) 0 + 0x >= 0 + 2x permute(true(), x, b()) -> 0() 0 + 1x >= 0 permute(false(), x, b()) -> permute(ack(x, x), p x, c()) 0 + 1x >= 2 + 1x permute(y, x, c()) -> s s permute(x, y, a()) 0 + 1x + 1y >= 2 + 1x + 1y permute(x, y, a()) -> permute(isZero x, x, b()) 0 + 1x + 1y >= 0 + 2x SCCS (1): Scc: {plus#(s x, y) -> plus#(x, s y)} SCC (1): Strict: {plus#(s x, y) -> plus#(x, s y)} Weak: { permute(x, y, a()) -> permute(isZero x, x, b()), permute(y, x, c()) -> s s permute(x, y, a()), permute(false(), x, b()) -> permute(ack(x, x), p x, c()), permute(true(), x, b()) -> 0(), double x -> permute(x, x, a()), isZero 0() -> true(), isZero s x -> false(), ack(0(), x) -> plus(x, s 0()), ack(s x, 0()) -> ack(x, s 0()), ack(s x, s y) -> ack(x, ack(s x, y)), p 0() -> 0(), p s x -> x, plus(x, 0()) -> x, plus(x, s 0()) -> s x, plus(x, s s y) -> s plus(s x, y), plus(0(), y) -> y, plus(s x, y) -> plus(x, s y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [permute](x0, x1, x2) = x0 + x1, [ack](x0, x1) = 1, [plus](x0, x1) = 0, [double](x0) = 0, [isZero](x0) = x0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [a] = 0, [b] = 0, [c] = 0, [false] = 0, [0] = 0, [true] = 0, [plus#](x0, x1) = x0 + 1 Strict: plus#(s x, y) -> plus#(x, s y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: plus(s x, y) -> plus(x, s y) 0 + 0x + 0y >= 0 + 0x + 0y plus(0(), y) -> y 0 + 0y >= 1y plus(x, s s y) -> s plus(s x, y) 0 + 0x + 0y >= 1 + 0x + 0y plus(x, s 0()) -> s x 0 + 0x >= 1 + 1x plus(x, 0()) -> x 0 + 0x >= 1x p s x -> x 2 + 1x >= 1x p 0() -> 0() 1 >= 0 ack(s x, s y) -> ack(x, ack(s x, y)) 1 + 0x + 0y >= 1 + 0x + 0y ack(s x, 0()) -> ack(x, s 0()) 1 + 0x >= 1 + 0x ack(0(), x) -> plus(x, s 0()) 1 + 0x >= 0 + 0x isZero s x -> false() 1 + 1x >= 0 isZero 0() -> true() 0 >= 0 double x -> permute(x, x, a()) 0 + 0x >= 0 + 2x permute(true(), x, b()) -> 0() 0 + 1x >= 0 permute(false(), x, b()) -> permute(ack(x, x), p x, c()) 0 + 1x >= 2 + 1x permute(y, x, c()) -> s s permute(x, y, a()) 0 + 1x + 1y >= 2 + 1x + 1y permute(x, y, a()) -> permute(isZero x, x, b()) 0 + 1x + 1y >= 0 + 2x Qed