YES Time: 0.031629 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) -> ifMinus(le(s X, Y), s X, Y), ifMinus(true(), s X, Y) -> 0(), ifMinus(false(), s X, Y) -> s minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y)} DP: DP: { le#(s X, s Y) -> le#(X, Y), minus#(s X, Y) -> le#(s X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y), quot#(s X, s Y) -> minus#(X, Y), quot#(s X, s Y) -> quot#(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) -> ifMinus(le(s X, Y), s X, Y), ifMinus(true(), s X, Y) -> 0(), ifMinus(false(), s X, Y) -> s minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y)} UR: { 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) -> ifMinus(le(s X, Y), s X, Y), ifMinus(true(), s X, Y) -> 0(), ifMinus(false(), s X, Y) -> s minus(X, Y), a(x, y) -> x, a(x, y) -> y} EDG: {(ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y)) (minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y)) (minus#(s X, Y) -> le#(s X, Y), le#(s X, s Y) -> le#(X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))} EDG: {(ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y)) (minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y)) (minus#(s X, Y) -> le#(s X, Y), le#(s X, s Y) -> le#(X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))} EDG: {(ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y)) (minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y)) (minus#(s X, Y) -> le#(s X, Y), le#(s X, s Y) -> le#(X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))} EDG: {(ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (ifMinus#(false(), s X, Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> quot#(minus(X, Y), s Y)) (quot#(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(s X, s Y) -> minus#(X, Y)) (minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y)) (minus#(s X, Y) -> le#(s X, Y), le#(s X, s Y) -> le#(X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> le#(s X, Y)) (quot#(s X, s Y) -> minus#(X, Y), minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y)) (le#(s X, s Y) -> le#(X, Y), le#(s X, s Y) -> le#(X, Y))} STATUS: arrows: 0.750000 SCCS (3): Scc: {quot#(s X, s Y) -> quot#(minus(X, Y), s Y)} Scc: { minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(false(), s X, Y) -> minus#(X, Y)} Scc: {le#(s X, s Y) -> le#(X, Y)} SCC (1): Strict: {quot#(s X, s Y) -> quot#(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) -> ifMinus(le(s X, Y), s X, Y), ifMinus(true(), s X, Y) -> 0(), ifMinus(false(), s X, Y) -> s minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifMinus](x0, x1, x2) = x0, [le](x0, x1) = 0, [minus](x0, x1) = x0, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [true] = 0, [0] = 0, [false] = 0, [quot#](x0, x1) = x0 + 1 Strict: quot#(s X, s Y) -> quot#(minus(X, Y), s Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 1Y + 0X >= 3 + 1Y + 0X quot(0(), s Y) -> 0() 2 + 1Y >= 0 ifMinus(false(), s X, Y) -> s minus(X, Y) 1 + 0Y + 1X >= 1 + 0Y + 1X ifMinus(true(), s X, Y) -> 0() 1 + 0Y + 1X >= 0 minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y) 1 + 0Y + 1X >= 1 + 0Y + 1X minus(0(), Y) -> 0() 0 + 0Y >= 0 le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 0Y >= 0 Qed SCC (2): Strict: { minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y), ifMinus#(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) -> ifMinus(le(s X, Y), s X, Y), ifMinus(true(), s X, Y) -> 0(), ifMinus(false(), s X, Y) -> s minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifMinus](x0, x1, x2) = 0, [le](x0, x1) = 0, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [ifMinus#](x0, x1, x2) = x0, [minus#](x0, x1) = x0 Strict: ifMinus#(false(), s X, Y) -> minus#(X, Y) 1 + 0Y + 1X >= 0 + 0Y + 1X minus#(s X, Y) -> ifMinus#(le(s X, Y), s X, Y) 1 + 0Y + 1X >= 1 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 1Y + 1X >= 3 + 1Y + 1X quot(0(), s Y) -> 0() 2 + 1Y >= 1 ifMinus(false(), s X, Y) -> s minus(X, Y) 0 + 0Y + 0X >= 2 + 0Y + 1X ifMinus(true(), s X, Y) -> 0() 0 + 0Y + 0X >= 1 minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y) 2 + 0Y + 1X >= 0 + 0Y + 0X minus(0(), Y) -> 0() 2 + 0Y >= 1 le(s X, s Y) -> le(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X le(s X, 0()) -> false() 0 + 0X >= 0 le(0(), Y) -> true() 0 + 0Y >= 0 SCCS (0): 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) -> ifMinus(le(s X, Y), s X, Y), ifMinus(true(), s X, Y) -> 0(), ifMinus(false(), s X, Y) -> s minus(X, Y), quot(0(), s Y) -> 0(), quot(s X, s Y) -> s quot(minus(X, Y), s Y)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [ifMinus](x0, x1, x2) = x0, [le](x0, x1) = x0 + 1, [minus](x0, x1) = x0 + 1, [quot](x0, x1) = x0 + 1, [s](x0) = x0 + 1, [true] = 0, [0] = 1, [false] = 0, [le#](x0, x1) = x0 + 1 Strict: le#(s X, s Y) -> le#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: quot(s X, s Y) -> s quot(minus(X, Y), s Y) 2 + 1Y + 0X >= 3 + 1Y + 0X quot(0(), s Y) -> 0() 2 + 1Y >= 1 ifMinus(false(), s X, Y) -> s minus(X, Y) 0 + 0Y + 0X >= 2 + 0Y + 1X ifMinus(true(), s X, Y) -> 0() 0 + 0Y + 0X >= 1 minus(s X, Y) -> ifMinus(le(s X, Y), s X, Y) 2 + 0Y + 1X >= 2 + 0Y + 1X minus(0(), Y) -> 0() 2 + 0Y >= 1 le(s X, s Y) -> le(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X le(s X, 0()) -> false() 2 + 1X >= 0 le(0(), Y) -> true() 2 + 0Y >= 0 Qed