YES Time: 0.014211 TRS: { perfectp 0() -> false(), perfectp s x -> f(x, s 0(), s x, s x), f(0(), y, 0(), u) -> true(), f(0(), y, s z, u) -> false(), f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u), f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))} DP: DP: { perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)} TRS: { perfectp 0() -> false(), perfectp s x -> f(x, s 0(), s x, s x), f(0(), y, 0(), u) -> true(), f(0(), y, s z, u) -> false(), f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u), f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))} UR: {a(w, v) -> w, a(w, v) -> v} EDG: {(f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(x, u, z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u))} EDG: {(f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(x, u, z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u))} EDG: {(f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(x, u, z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u))} EDG: {(f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(x, u, z, u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(x, u, z, u)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u))} STATUS: arrows: 0.500000 SCCS (1): Scc: {f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u)} SCC (2): Strict: {f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u), f#(s x, s y, z, u) -> f#(x, u, z, u)} Weak: { perfectp 0() -> false(), perfectp s x -> f(x, s 0(), s x, s x), f(0(), y, 0(), u) -> true(), f(0(), y, s z, u) -> false(), f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u), f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1, x2, x3) = x0 + x1 + x2, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [minus](x0, x1) = x0, [le](x0, x1) = x0 + 1, [perfectp](x0) = x0 + 1, [s](x0) = x0 + 1, [false] = 0, [0] = 1, [true] = 0, [f#](x0, x1, x2, x3) = x0 Strict: f#(s x, s y, z, u) -> f#(x, u, z, u) 1 + 1x + 0y + 0u + 0z >= 0 + 1x + 0u + 0z f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u) 1 + 1x + 0u + 0z >= 0 + 1x + 0u + 0z Weak: f(s x, s y, z, u) -> if(le(x, y), f(s x, minus(y, x), z, u), f(x, u, z, u)) 2 + 1x + 1y + 1u + 0z >= 3 + 2x + 2y + 3u + 0z f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u) 2 + 1x + 1u + 0z >= 0 + 1x + 2u + 0z f(0(), y, s z, u) -> false() 1 + 1y + 1u + 0z >= 0 f(0(), y, 0(), u) -> true() 1 + 1y + 1u >= 0 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 3 + 2x perfectp 0() -> false() 2 >= 0 Qed