MAYBE Time: 0.175525 TRS: { minus(x, x) -> 0(), minus(x, 0()) -> x, minus(0(), x) -> 0(), 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_quot(x, y, true(), z) -> divByZeroError(), if_quot(x, y, false(), true()) -> s quot(x, y), if_quot(x, y, false(), false()) -> 0(), quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))} DP: DP: { minus#(s x, s y) -> minus#(x, y), le#(s x, s y) -> le#(x, y), if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> minus#(x, y), quot#(x, y) -> le#(y, x), quot#(x, y) -> le#(y, 0()), quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))} TRS: { minus(x, x) -> 0(), minus(x, 0()) -> x, minus(0(), x) -> 0(), 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_quot(x, y, true(), z) -> divByZeroError(), if_quot(x, y, false(), true()) -> s quot(x, y), if_quot(x, y, false(), false()) -> 0(), quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))} UR: { minus(x, x) -> 0(), minus(x, 0()) -> x, minus(0(), x) -> 0(), 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), a(w, v) -> w, a(w, v) -> v} EDG: {(quot#(x, y) -> le#(y, x), le#(s x, s y) -> le#(x, y)) (minus#(s x, s y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))) (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> le#(y, 0())) (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> le#(y, x)) (if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> minus#(x, y)) (quot#(x, y) -> minus#(x, y), minus#(s x, s y) -> minus#(x, y)) (le#(s x, s y) -> le#(x, y), le#(s x, s y) -> le#(x, y)) (quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x)), if_quot#(x, y, false(), true()) -> quot#(x, y))} STATUS: arrows: 0.816327 SCCS (3): Scc: {if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))} Scc: {minus#(s x, s y) -> minus#(x, y)} Scc: {le#(s x, s y) -> le#(x, y)} SCC (2): Strict: {if_quot#(x, y, false(), true()) -> quot#(x, y), quot#(x, y) -> if_quot#(minus(x, y), y, le(y, 0()), le(y, x))} Weak: { minus(x, x) -> 0(), minus(x, 0()) -> x, minus(0(), x) -> 0(), 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_quot(x, y, true(), z) -> divByZeroError(), if_quot(x, y, false(), true()) -> s quot(x, y), if_quot(x, y, false(), false()) -> 0(), quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))} Fail SCC (1): Strict: {minus#(s x, s y) -> minus#(x, y)} Weak: { minus(x, x) -> 0(), minus(x, 0()) -> x, minus(0(), x) -> 0(), 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_quot(x, y, true(), z) -> divByZeroError(), if_quot(x, y, false(), true()) -> s quot(x, y), if_quot(x, y, false(), false()) -> 0(), quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_quot](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [minus](x0, x1) = x0 + x1 + 1, [le](x0, x1) = x0 + 1, [quot](x0, x1) = 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 0, [divByZeroError] = 0, [minus#](x0, x1) = x0 Strict: minus#(s x, s y) -> minus#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x)) 1 + 0x + 0y >= 3 + 0x + 3y if_quot(x, y, false(), false()) -> 0() 1 + 0x + 1y >= 1 if_quot(x, y, false(), true()) -> s quot(x, y) 2 + 0x + 1y >= 2 + 0x + 0y if_quot(x, y, true(), z) -> divByZeroError() 2 + 0x + 1y + 1z >= 0 le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 1 minus(s x, s y) -> minus(x, y) 3 + 1x + 1y >= 1 + 1x + 1y minus(0(), x) -> 0() 2 + 1x >= 1 minus(x, 0()) -> x 2 + 1x >= 1x minus(x, x) -> 0() 1 + 2x >= 1 Qed SCC (1): Strict: {le#(s x, s y) -> le#(x, y)} Weak: { minus(x, x) -> 0(), minus(x, 0()) -> x, minus(0(), x) -> 0(), 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_quot(x, y, true(), z) -> divByZeroError(), if_quot(x, y, false(), true()) -> s quot(x, y), if_quot(x, y, false(), false()) -> 0(), quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if_quot](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [minus](x0, x1) = x0 + x1 + 1, [le](x0, x1) = x0 + 1, [quot](x0, x1) = 1, [s](x0) = x0 + 1, [0] = 1, [true] = 1, [false] = 0, [divByZeroError] = 0, [le#](x0, x1) = x0 Strict: le#(s x, s y) -> le#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y Weak: quot(x, y) -> if_quot(minus(x, y), y, le(y, 0()), le(y, x)) 1 + 0x + 0y >= 3 + 0x + 3y if_quot(x, y, false(), false()) -> 0() 1 + 0x + 1y >= 1 if_quot(x, y, false(), true()) -> s quot(x, y) 2 + 0x + 1y >= 2 + 0x + 0y if_quot(x, y, true(), z) -> divByZeroError() 2 + 0x + 1y + 1z >= 0 le(s x, s y) -> le(x, y) 2 + 1x + 0y >= 1 + 1x + 0y le(s x, 0()) -> false() 2 + 1x >= 0 le(0(), y) -> true() 2 + 0y >= 1 minus(s x, s y) -> minus(x, y) 3 + 1x + 1y >= 1 + 1x + 1y minus(0(), x) -> 0() 2 + 1x >= 1 minus(x, 0()) -> x 2 + 1x >= 1x minus(x, x) -> 0() 1 + 2x >= 1 Qed