YES Time: 3.411583 TRS: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))} DP: DP: { -#(s x, s y) -> -#(x, y), <=#(s x, s y) -> <=#(x, y), perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, 0(), z, u) -> -#(z, s x), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> -#(y, x), f#(s x, s y, z, u) -> <=#(x, y), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), 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, -(y, x), z, u)} TRS: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))} UR: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, f(0(), y, 0(), u) -> true(), f(0(), y, s z, u) -> false(), f(s x, 0(), z, u) -> f(x, u, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)), a(w, v) -> w, a(w, v) -> v} EDG: {(perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> f#(s x, -(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) -> if#(<=(x, y), f(s x, -(y, x), 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) -> <=#(x, y)) (perfectp# s x -> f#(x, s 0(), s x, s x), f#(s x, s y, z, u) -> -#(y, x)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> f#(s x, -(y, x), 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#(x, u, z, u), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), 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) -> <=#(x, y)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, s y, z, u) -> -#(y, x)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u)) (f#(s x, s y, z, u) -> f#(x, u, z, u), f#(s x, 0(), z, u) -> -#(z, s x)) (-#(s x, s y) -> -#(x, y), -#(s x, s y) -> -#(x, y)) (f#(s x, s y, z, u) -> <=#(x, y), <=#(s x, s y) -> <=#(x, y)) (f#(s x, s y, z, u) -> -#(y, x), -#(s x, s y) -> -#(x, y)) (<=#(s x, s y) -> <=#(x, y), <=#(s x, s y) -> <=#(x, y)) (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, 0(), z, u) -> -#(z, s x)) (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u)) (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> -#(y, x)) (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> <=#(x, y)) (f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))) (f#(s x, s y, z, u) -> f#(s x, -(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, -(y, x), z, u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)) (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, 0(), z, u) -> -#(z, s x)) (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u)) (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> -#(y, x)) (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> <=#(x, y)) (f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> if#(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u))) (f#(s x, 0(), z, u) -> f#(x, u, -(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, -(z, s x), u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)) (f#(s x, 0(), z, u) -> -#(z, s x), -#(s x, s y) -> -#(x, y))} STATUS: arrows: 0.690000 SCCS (3): Scc: {f#(s x, 0(), z, u) -> f#(x, u, -(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, -(y, x), z, u)} Scc: {<=#(s x, s y) -> <=#(x, y)} Scc: {-#(s x, s y) -> -#(x, y)} SCC (3): Strict: {f#(s x, 0(), z, u) -> f#(x, u, -(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, -(y, x), z, u)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(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, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [-](x0, x1) = x0 + 1, [<=](x0, x1) = 0, [s](x0) = x0 + 1, [perfectp](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [f#](x0, x1, x2, x3) = x0 + x1 + 1 Strict: f#(s x, s y, z, u) -> f#(s x, -(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, -(z, s x), u) 2 + 1x + 0u + 1z >= 2 + 1x + 0u + 1z Weak: f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)) 2 + 1x + 1y + 0u + 0z >= 3 + 2x + 1y + 1u + 0z f(s x, 0(), z, u) -> f(x, u, -(z, s x), u) 2 + 1x + 0u + 0z >= 0 + 1x + 1u + 0z f(0(), y, s z, u) -> false() 1 + 1y + 0u + 0z >= 1 f(0(), y, 0(), u) -> true() 1 + 1y + 0u >= 1 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 2 + 1x perfectp 0() -> false() 2 >= 1 if(false(), x, y) -> y 2 + 1x + 1y >= 1y if(true(), x, y) -> x 2 + 1x + 1y >= 1x <=(s x, s y) -> <=(x, y) 0 + 0x + 0y >= 0 + 0x + 0y <=(s x, 0()) -> false() 0 + 0x >= 1 <=(0(), y) -> true() 0 + 0y >= 1 -(s x, s y) -> -(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -(x, 0()) -> x 1 + 1x >= 1x SCCS (1): Scc: {f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)} SCC (2): Strict: {f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u), f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(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, [if](x0, x1, x2) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [<=](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [perfectp](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [f#](x0, x1, x2, x3) = x0 + 1 Strict: f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u) 2 + 1x + 0y + 0u + 0z >= 2 + 1x + 0y + 0u + 0z f#(s x, 0(), z, u) -> f#(x, u, -(z, s x), u) 2 + 1x + 0u + 0z >= 1 + 1x + 0u + 0z Weak: f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)) 2 + 1x + 1y + 0u + 0z >= 4 + 3x + 0y + 0u + 0z f(s x, 0(), z, u) -> f(x, u, -(z, s x), u) 2 + 1x + 0u + 0z >= 0 + 1x + 1u + 0z f(0(), y, s z, u) -> false() 1 + 1y + 0u + 0z >= 1 f(0(), y, 0(), u) -> true() 1 + 1y + 0u >= 1 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 2 + 1x perfectp 0() -> false() 2 >= 1 if(false(), x, y) -> y 2 + 1x + 0y >= 1y if(true(), x, y) -> x 2 + 1x + 0y >= 1x <=(s x, s y) -> <=(x, y) 2 + 1x + 0y >= 1 + 1x + 0y <=(s x, 0()) -> false() 2 + 1x >= 1 <=(0(), y) -> true() 2 + 0y >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x SCCS (1): Scc: {f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)} SCC (1): Strict: {f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(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, [if](x0, x1, x2) = x0 + 1, [-](x0, x1) = x0, [<=](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [perfectp](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [f#](x0, x1, x2, x3) = x0 + x1 + 1 Strict: f#(s x, s y, z, u) -> f#(s x, -(y, x), z, u) 3 + 1x + 1y + 0u + 0z >= 2 + 1x + 1y + 0u + 0z Weak: f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)) 1 + 0x + 1y + 0u + 0z >= 2 + 1x + 0y + 0u + 0z f(s x, 0(), z, u) -> f(x, u, -(z, s x), u) 1 + 0x + 0u + 0z >= 0 + 0x + 1u + 0z f(0(), y, s z, u) -> false() 0 + 1y + 0u + 0z >= 1 f(0(), y, 0(), u) -> true() 0 + 1y + 0u >= 1 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 2 + 0x perfectp 0() -> false() 2 >= 1 if(false(), x, y) -> y 2 + 0x + 0y >= 1y if(true(), x, y) -> x 2 + 0x + 0y >= 1x <=(s x, s y) -> <=(x, y) 2 + 1x + 0y >= 1 + 1x + 0y <=(s x, 0()) -> false() 2 + 1x >= 1 <=(0(), y) -> true() 2 + 0y >= 1 -(s x, s y) -> -(x, y) 1 + 1x + 0y >= 0 + 1x + 0y -(x, 0()) -> x 0 + 1x >= 1x Qed SCC (1): Strict: {<=#(s x, s y) -> <=#(x, y)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(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, [if](x0, x1, x2) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [<=](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [perfectp](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [<=#](x0, x1) = x0 Strict: <=#(s x, s y) -> <=#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)) 1 + 0x + 1y + 0u + 0z >= 2 + 1x + 0y + 1u + 0z f(s x, 0(), z, u) -> f(x, u, -(z, s x), u) 1 + 0x + 0u + 0z >= 0 + 0x + 1u + 0z f(0(), y, s z, u) -> false() 0 + 1y + 0u + 0z >= 1 f(0(), y, 0(), u) -> true() 0 + 1y + 0u >= 1 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 2 + 0x perfectp 0() -> false() 2 >= 1 if(false(), x, y) -> y 2 + 0x + 1y >= 1y if(true(), x, y) -> x 2 + 0x + 1y >= 1x <=(s x, s y) -> <=(x, y) 2 + 1x + 0y >= 1 + 1x + 0y <=(s x, 0()) -> false() 2 + 1x >= 1 <=(0(), y) -> true() 2 + 0y >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x Qed SCC (1): Strict: {-#(s x, s y) -> -#(x, y)} Weak: { -(x, 0()) -> x, -(s x, s y) -> -(x, y), <=(0(), y) -> true(), <=(s x, 0()) -> false(), <=(s x, s y) -> <=(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, 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, -(z, s x), u), f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(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, [if](x0, x1, x2) = x0 + x1 + 1, [-](x0, x1) = x0 + 1, [<=](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [perfectp](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 1, [-#](x0, x1) = x0 Strict: -#(s x, s y) -> -#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: f(s x, s y, z, u) -> if(<=(x, y), f(s x, -(y, x), z, u), f(x, u, z, u)) 1 + 0x + 1y + 0u + 0z >= 2 + 1x + 0y + 1u + 0z f(s x, 0(), z, u) -> f(x, u, -(z, s x), u) 1 + 0x + 0u + 0z >= 0 + 0x + 1u + 0z f(0(), y, s z, u) -> false() 0 + 1y + 0u + 0z >= 1 f(0(), y, 0(), u) -> true() 0 + 1y + 0u >= 1 perfectp s x -> f(x, s 0(), s x, s x) 2 + 1x >= 2 + 0x perfectp 0() -> false() 2 >= 1 if(false(), x, y) -> y 2 + 0x + 1y >= 1y if(true(), x, y) -> x 2 + 0x + 1y >= 1x <=(s x, s y) -> <=(x, y) 2 + 1x + 0y >= 1 + 1x + 0y <=(s x, 0()) -> false() 2 + 1x >= 1 <=(0(), y) -> true() 2 + 0y >= 1 -(s x, s y) -> -(x, y) 2 + 0x + 1y >= 1 + 0x + 1y -(x, 0()) -> x 2 + 0x >= 1x Qed