MAYBE Time: 0.062253 TRS: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(eq(x, y), x, y), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y) -> cond2(gr(x, y), x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y), eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y)} DP: DP: { cond2#(true(), x, y) -> gr#(add(x, y), 0()), cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond2#(true(), x, y) -> add#(x, y), cond2#(true(), x, y) -> p# x, cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond2#(false(), x, y) -> eq#(x, y), gr#(s x, s y) -> gr#(x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond1#(true(), x, y) -> gr#(x, y), add#(s x, y) -> add#(x, y), cond3#(true(), x, y) -> gr#(add(x, y), 0()), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond3#(true(), x, y) -> add#(x, y), cond3#(true(), x, y) -> p# x, cond3#(false(), x, y) -> gr#(add(x, y), 0()), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond3#(false(), x, y) -> add#(x, y), cond3#(false(), x, y) -> p# y, eq#(s x, s y) -> eq#(x, y)} TRS: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(eq(x, y), x, y), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y) -> cond2(gr(x, y), x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y), eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y)} UR: { gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y), a(z, w) -> z, a(z, w) -> w} EDG: {(cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond1#(true(), x, y) -> gr#(x, y)) (cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y)) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(false(), x, y) -> p# y) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(false(), x, y) -> add#(x, y)) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y)) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(false(), x, y) -> gr#(add(x, y), 0())) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(true(), x, y) -> p# x) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(true(), x, y) -> add#(x, y)) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y)) (cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond3#(true(), x, y) -> gr#(add(x, y), 0())) (gr#(s x, s y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y)) (cond1#(true(), x, y) -> gr#(x, y), gr#(s x, s y) -> gr#(x, y)) (cond3#(true(), x, y) -> add#(x, y), add#(s x, y) -> add#(x, y)) (eq#(s x, s y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y)) (cond3#(false(), x, y) -> add#(x, y), add#(s x, y) -> add#(x, y)) (add#(s x, y) -> add#(x, y), add#(s x, y) -> add#(x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> gr#(add(x, y), 0())) (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> add#(x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(true(), x, y) -> p# x) (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> cond3#(eq(x, y), x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond2#(false(), x, y) -> eq#(x, y)) (cond2#(false(), x, y) -> eq#(x, y), eq#(s x, s y) -> eq#(x, y)) (cond2#(true(), x, y) -> add#(x, y), add#(s x, y) -> add#(x, y)) (cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y)) (cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond1#(true(), x, y) -> gr#(x, y)) (cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y)) (cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond1#(true(), x, y) -> gr#(x, y))} STATUS: arrows: 0.922438 SCCS (4): Scc: { cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y)} Scc: {eq#(s x, s y) -> eq#(x, y)} Scc: {add#(s x, y) -> add#(x, y)} Scc: {gr#(s x, s y) -> gr#(x, y)} SCC (5): Strict: { cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond2#(false(), x, y) -> cond3#(eq(x, y), x, y), cond1#(true(), x, y) -> cond2#(gr(x, y), x, y), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y)} Weak: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(eq(x, y), x, y), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y) -> cond2(gr(x, y), x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y), eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y)} Fail SCC (1): Strict: {eq#(s x, s y) -> eq#(x, y)} Weak: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(eq(x, y), x, y), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y) -> cond2(gr(x, y), x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y), eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cond2](x0, x1, x2) = x0 + x1 + x2 + 1, [cond1](x0, x1, x2) = 0, [cond3](x0, x1, x2) = x0 + x1 + x2, [gr](x0, x1) = x0 + x1 + 1, [add](x0, x1) = 0, [eq](x0, x1) = x0 + x1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [true] = 1, [0] = 1, [false] = 1, [eq#](x0, x1) = x0 Strict: eq#(s x, s y) -> eq#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: eq(s x, s y) -> eq(x, y) 2 + 1x + 1y >= 0 + 1x + 1y eq(s x, 0()) -> false() 2 + 1x >= 1 eq(0(), s x) -> false() 2 + 1x >= 1 eq(0(), 0()) -> true() 2 >= 1 cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y) 1 + 1x + 1y >= 0 + 0x + 0y cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 1 + 1x + 1y >= 0 + 0x + 0y p s x -> x 2 + 1x >= 1x p 0() -> 0() 2 >= 1 add(s x, y) -> s add(x, y) 0 + 0x + 0y >= 1 + 0x + 0y add(0(), x) -> x 0 + 0x >= 1x cond1(true(), x, y) -> cond2(gr(x, y), x, y) 0 + 0x + 0y >= 2 + 2x + 2y gr(s x, s y) -> gr(x, y) 3 + 1x + 1y >= 1 + 1x + 1y gr(s x, 0()) -> true() 3 + 1x >= 1 gr(0(), x) -> false() 2 + 1x >= 1 cond2(false(), x, y) -> cond3(eq(x, y), x, y) 2 + 1x + 1y >= 0 + 2x + 2y cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 2 + 1x + 1y >= 0 + 0x + 0y Qed SCC (1): Strict: {add#(s x, y) -> add#(x, y)} Weak: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(eq(x, y), x, y), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y) -> cond2(gr(x, y), x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y), eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cond2](x0, x1, x2) = x0 + x1 + x2 + 1, [cond1](x0, x1, x2) = 0, [cond3](x0, x1, x2) = x0 + x1 + x2 + 1, [gr](x0, x1) = x0 + x1 + 1, [add](x0, x1) = 0, [eq](x0, x1) = x0 + x1 + 1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [true] = 1, [0] = 1, [false] = 1, [add#](x0, x1) = x0 Strict: add#(s x, y) -> add#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: eq(s x, s y) -> eq(x, y) 3 + 1x + 1y >= 1 + 1x + 1y eq(s x, 0()) -> false() 3 + 1x >= 1 eq(0(), s x) -> false() 3 + 1x >= 1 eq(0(), 0()) -> true() 3 >= 1 cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y) 2 + 1x + 1y >= 0 + 0x + 0y cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 2 + 1x + 1y >= 0 + 0x + 0y p s x -> x 2 + 1x >= 1x p 0() -> 0() 2 >= 1 add(s x, y) -> s add(x, y) 0 + 0x + 0y >= 1 + 0x + 0y add(0(), x) -> x 0 + 0x >= 1x cond1(true(), x, y) -> cond2(gr(x, y), x, y) 0 + 0x + 0y >= 2 + 2x + 2y gr(s x, s y) -> gr(x, y) 3 + 1x + 1y >= 1 + 1x + 1y gr(s x, 0()) -> true() 3 + 1x >= 1 gr(0(), x) -> false() 2 + 1x >= 1 cond2(false(), x, y) -> cond3(eq(x, y), x, y) 2 + 1x + 1y >= 2 + 2x + 2y cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 2 + 1x + 1y >= 0 + 0x + 0y Qed SCC (1): Strict: {gr#(s x, s y) -> gr#(x, y)} Weak: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(eq(x, y), x, y), gr(0(), x) -> false(), gr(s x, 0()) -> true(), gr(s x, s y) -> gr(x, y), cond1(true(), x, y) -> cond2(gr(x, y), x, y), add(0(), x) -> x, add(s x, y) -> s add(x, y), p 0() -> 0(), p s x -> x, cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y), eq(0(), 0()) -> true(), eq(0(), s x) -> false(), eq(s x, 0()) -> false(), eq(s x, s y) -> eq(x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cond2](x0, x1, x2) = x0 + x1 + x2 + 1, [cond1](x0, x1, x2) = 0, [cond3](x0, x1, x2) = x0 + x1 + x2, [gr](x0, x1) = x0 + x1 + 1, [add](x0, x1) = 0, [eq](x0, x1) = x0 + x1, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [true] = 1, [0] = 1, [false] = 1, [gr#](x0, x1) = x0 Strict: gr#(s x, s y) -> gr#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: eq(s x, s y) -> eq(x, y) 2 + 1x + 1y >= 0 + 1x + 1y eq(s x, 0()) -> false() 2 + 1x >= 1 eq(0(), s x) -> false() 2 + 1x >= 1 eq(0(), 0()) -> true() 2 >= 1 cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, p y) 1 + 1x + 1y >= 0 + 0x + 0y cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 1 + 1x + 1y >= 0 + 0x + 0y p s x -> x 2 + 1x >= 1x p 0() -> 0() 2 >= 1 add(s x, y) -> s add(x, y) 0 + 0x + 0y >= 1 + 0x + 0y add(0(), x) -> x 0 + 0x >= 1x cond1(true(), x, y) -> cond2(gr(x, y), x, y) 0 + 0x + 0y >= 2 + 2x + 2y gr(s x, s y) -> gr(x, y) 3 + 1x + 1y >= 1 + 1x + 1y gr(s x, 0()) -> true() 3 + 1x >= 1 gr(0(), x) -> false() 2 + 1x >= 1 cond2(false(), x, y) -> cond3(eq(x, y), x, y) 2 + 1x + 1y >= 0 + 2x + 2y cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 2 + 1x + 1y >= 0 + 0x + 0y Qed