MAYBE Time: 0.039503 TRS: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(gr(y, 0()), 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, 0()), 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()), x, p y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), 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) -> gr#(y, 0()), cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), gr#(s x, s y) -> gr#(x, y), cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond1#(true(), x, y) -> gr#(x, 0()), 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()), x, p y), cond3#(true(), x, y) -> add#(x, y), cond3#(true(), x, y) -> p# y, cond3#(false(), x, y) -> gr#(add(x, y), 0()), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, y), cond3#(false(), x, y) -> add#(x, y)} TRS: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(gr(y, 0()), 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, 0()), 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()), x, p y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, y)} EDG: {(cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(false(), x, y) -> add#(x, y)) (cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, y)) (cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(false(), x, y) -> gr#(add(x, y), 0())) (cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(true(), x, y) -> p# y) (cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(true(), x, y) -> add#(x, y)) (cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y)) (cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond3#(true(), x, y) -> gr#(add(x, y), 0())) (cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, y), cond1#(true(), x, y) -> gr#(x, 0())) (cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, y), cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y)) (cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond1#(true(), x, y) -> gr#(x, 0())) (cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y)) (gr#(s x, s 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)) (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)) (cond2#(true(), x, y) -> add#(x, y), add#(s x, y) -> add#(x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond2#(true(), x, y) -> gr#(add(x, y), 0())) (cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond2#(true(), x, y) -> add#(x, y)) (cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond2#(true(), x, y) -> p# x) (cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond2#(false(), x, y) -> gr#(y, 0())) (cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y)) (cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y)) (cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond1#(true(), x, y) -> gr#(x, 0()))} STATUS: arrows: 0.916955 SCCS (3): Scc: {gr#(s x, s y) -> gr#(x, y)} Scc: { cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, y)} Scc: {add#(s x, y) -> add#(x, y)} 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(gr(y, 0()), 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, 0()), 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()), x, p y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cond2](x0, x1, x2) = x0 + x1 + 1, [cond1](x0, x1, x2) = 0, [cond3](x0, x1, x2) = x0 + x1, [gr](x0, x1) = x0 + x1 + 1, [add](x0, x1) = 0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [gr#](x0, x1) = x0 Strict: gr#(s x, s y) -> gr#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, y) 1 + 0x + 1y >= 0 + 0x + 0y cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), x, p y) 1 + 0x + 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, 0()), x, y) 0 + 0x + 0y >= 3 + 2x + 0y 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(gr(y, 0()), x, y) 2 + 1x + 0y >= 2 + 0x + 2y cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 2 + 1x + 0y >= 0 + 0x + 0y Qed SCC (5): Strict: { cond2#(true(), x, y) -> cond1#(gr(add(x, y), 0()), p x, y), cond2#(false(), x, y) -> cond3#(gr(y, 0()), x, y), cond1#(true(), x, y) -> cond2#(gr(x, 0()), x, y), cond3#(true(), x, y) -> cond1#(gr(add(x, y), 0()), x, p y), cond3#(false(), x, y) -> cond1#(gr(add(x, y), 0()), x, y)} Weak: { cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y), cond2(false(), x, y) -> cond3(gr(y, 0()), 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, 0()), 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()), x, p y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, y)} Fail 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(gr(y, 0()), 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, 0()), 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()), x, p y), cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cond2](x0, x1, x2) = x0 + x1 + 1, [cond1](x0, x1, x2) = 0, [cond3](x0, x1, x2) = x0 + x1, [gr](x0, x1) = x0 + x1 + 1, [add](x0, x1) = 0, [p](x0) = x0 + 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [add#](x0, x1) = x0 Strict: add#(s x, y) -> add#(x, y) 1 + 1x + 0y >= 0 + 1x + 0y Weak: cond3(false(), x, y) -> cond1(gr(add(x, y), 0()), x, y) 1 + 0x + 1y >= 0 + 0x + 0y cond3(true(), x, y) -> cond1(gr(add(x, y), 0()), x, p y) 1 + 0x + 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, 0()), x, y) 0 + 0x + 0y >= 3 + 2x + 0y 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(gr(y, 0()), x, y) 2 + 1x + 0y >= 2 + 0x + 2y cond2(true(), x, y) -> cond1(gr(add(x, y), 0()), p x, y) 2 + 1x + 0y >= 0 + 0x + 0y Qed