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