YES Time: 0.019145 TRS: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), mod(0(), y) -> 0(), mod(s x, 0()) -> 0(), mod(s x, s y) -> if_mod(le(y, x), s x, s y), if_mod(true(), s x, s y) -> mod(minus(x, y), s y), if_mod(false(), s x, s y) -> s x} DP: DP: { le#(s x, s y) -> le#(x, y), minus#(s x, y) -> le#(s x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y), mod#(s x, s y) -> le#(y, x), mod#(s x, s y) -> if_mod#(le(y, x), s x, s y), if_mod#(true(), s x, s y) -> minus#(x, y), if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y)} TRS: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), mod(0(), y) -> 0(), mod(s x, 0()) -> 0(), mod(s x, s y) -> if_mod(le(y, x), s x, s y), if_mod(true(), s x, s y) -> mod(minus(x, y), s y), if_mod(false(), s x, s y) -> s x} EDG: {(mod#(s x, s y) -> le#(y, x), le#(s x, s y) -> le#(x, y)) (if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y), mod#(s x, s y) -> if_mod#(le(y, x), s x, s y)) (if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y), mod#(s x, s y) -> le#(y, x)) (if_minus#(false(), s x, y) -> minus#(x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y)) (if_minus#(false(), s x, y) -> minus#(x, y), minus#(s x, y) -> le#(s x, y)) (if_mod#(true(), s x, s y) -> minus#(x, y), minus#(s x, y) -> if_minus#(le(s x, y), s x, y)) (if_mod#(true(), s x, s y) -> minus#(x, y), minus#(s x, y) -> le#(s x, y)) (mod#(s x, s y) -> if_mod#(le(y, x), s x, s y), if_mod#(true(), s x, s y) -> minus#(x, y)) (mod#(s x, s y) -> if_mod#(le(y, x), s x, s y), if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (minus#(s x, y) -> le#(s x, y), le#(s x, s y) -> le#(x, y)) (minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y))} SCCS (3): Scc: { mod#(s x, s y) -> if_mod#(le(y, x), s x, s y), if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y)} Scc: { minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y)} Scc: {le#(s x, s y) -> le#(x, y)} SCC (2): Strict: { mod#(s x, s y) -> if_mod#(le(y, x), s x, s y), if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), mod(0(), y) -> 0(), mod(s x, 0()) -> 0(), mod(s x, s y) -> if_mod(le(y, x), s x, s y), if_mod(true(), s x, s y) -> mod(minus(x, y), s y), if_mod(false(), s x, s y) -> s x} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_minus](x0, x1, x2) = x0, [if_mod](x0, x1, x2) = x0 + 1, [le](x0, x1) = 0, [minus](x0, x1) = x0, [mod](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [if_mod#](x0, x1, x2) = x0 + 1, [mod#](x0, x1) = x0 + 1 Strict: if_mod#(true(), s x, s y) -> mod#(minus(x, y), s y) 2 + 0y + 1x >= 1 + 0y + 1x mod#(s x, s y) -> if_mod#(le(y, x), s x, s y) 2 + 0y + 1x >= 2 + 0y + 1x Weak: EDG: {} SCCS (0): Qed SCC (2): Strict: { minus#(s x, y) -> if_minus#(le(s x, y), s x, y), if_minus#(false(), s x, y) -> minus#(x, y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), mod(0(), y) -> 0(), mod(s x, 0()) -> 0(), mod(s x, s y) -> if_mod(le(y, x), s x, s y), if_mod(true(), s x, s y) -> mod(minus(x, y), s y), if_mod(false(), s x, s y) -> s x} SPSC: Simple Projection: pi(if_minus#) = 1, pi(minus#) = 0 Strict: {minus#(s x, y) -> if_minus#(le(s x, y), s x, y)} EDG: {} SCCS (0): Qed SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { le(0(), y) -> true(), le(s x, 0()) -> false(), le(s x, s y) -> le(x, y), minus(0(), y) -> 0(), minus(s x, y) -> if_minus(le(s x, y), s x, y), if_minus(true(), s x, y) -> 0(), if_minus(false(), s x, y) -> s minus(x, y), mod(0(), y) -> 0(), mod(s x, 0()) -> 0(), mod(s x, s y) -> if_mod(le(y, x), s x, s y), if_mod(true(), s x, s y) -> mod(minus(x, y), s y), if_mod(false(), s x, s y) -> s x} SPSC: Simple Projection: pi(le#) = 1 Strict: {} Qed