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