YES Time: 0.095944 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))} STATUS: arrows: 0.250000 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), f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)} SCC (3): 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), f#(s x, s y, z, u) -> f#(s x, minus(y, x), 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 + 1, [if](x0, x1, x2) = x0 + 1, [minus](x0, x1) = 1, [le](x0, x1) = x0 + x1 + 1, [perfectp](x0) = 0, [s](x0) = x0 + 1, [false] = 0, [0] = 0, [true] = 0, [f#](x0, x1, x2, x3) = x0 + x1 + 1 Strict: f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u) 2 + 1x + 0y + 0u + 1z >= 2 + 1x + 0y + 0u + 1z f#(s x, s y, z, u) -> f#(x, u, z, u) 2 + 1x + 0y + 0u + 1z >= 1 + 1x + 0u + 1z f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u) 2 + 1x + 0u + 1z >= 2 + 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 + 0y + 0u + 1z >= 2 + 1x + 1y + 0u + 0z f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u) 2 + 1x + 0u + 1z >= 2 + 1x + 0u + 0z f(0(), y, s z, u) -> false() 2 + 0y + 0u + 1z >= 0 f(0(), y, 0(), u) -> true() 1 + 0y + 0u >= 0 perfectp s x -> f(x, s 0(), s x, s x) 0 + 0x >= 2 + 2x perfectp 0() -> false() 0 >= 0 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#(s x, minus(y, x), 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#(s x, minus(y, x), 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 + 1, [minus](x0, x1) = x0 + 1, [le](x0, x1) = x0 + x1 + 1, [perfectp](x0) = x0 + 1, [s](x0) = x0 + 1, [false] = 0, [0] = 1, [true] = 0, [f#](x0, x1, x2, x3) = x0 + 1 Strict: f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u) 2 + 1x + 0y + 0u + 0z >= 2 + 1x + 0y + 0u + 0z f#(s x, 0(), z, u) -> f#(x, u, minus(z, s x), u) 2 + 1x + 0u + 0z >= 1 + 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 + 0u + 1z >= 4 + 3x + 1y + 0u + 1z f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u) 2 + 1x + 0u + 1z >= 2 + 2x + 1u + 0z f(0(), y, s z, u) -> false() 2 + 1y + 0u + 1z >= 0 f(0(), y, 0(), u) -> true() 2 + 1y + 0u >= 0 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 3 + 2x perfectp 0() -> false() 2 >= 0 SCCS (1): Scc: {f#(s x, s y, z, u) -> f#(s x, minus(y, x), z, u)} SCC (1): Strict: {f#(s x, s y, z, u) -> f#(s x, minus(y, x), 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 + 1, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [minus](x0, x1) = 0, [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#(s x, minus(y, x), z, u) 1 + 0x + 1y + 0u + 0z >= 0 + 0x + 0y + 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 + 0y + 1u + 1z >= 5 + 3x + 0y + 2u + 2z f(s x, 0(), z, u) -> f(x, u, minus(z, s x), u) 2 + 1x + 1u + 1z >= 1 + 1x + 1u + 0z f(0(), y, s z, u) -> false() 3 + 0y + 1u + 1z >= 0 f(0(), y, 0(), u) -> true() 3 + 0y + 1u >= 0 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 3 + 3x perfectp 0() -> false() 2 >= 0 Qed