YES Time: 0.131167 TRS: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} DP: DP: { a__minus#(s X, s Y) -> a__minus#(X, Y), a__geq#(s X, s Y) -> a__geq#(X, Y), a__div#(s X, s Y) -> a__geq#(X, Y), a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2), mark# div(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(X1, X2), mark# geq(X1, X2) -> a__geq#(X1, X2), mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), mark# if(X1, X2, X3) -> mark# X1} TRS: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} UR: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3), a(x, y) -> x, a(x, y) -> y} EDG: {(a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(false(), X, Y) -> mark# Y) (a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X) (mark# geq(X1, X2) -> a__geq#(X1, X2), a__geq#(s X, s Y) -> a__geq#(X, Y)) (mark# div(X1, X2) -> a__div#(mark X1, X2), a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0())) (mark# div(X1, X2) -> a__div#(mark X1, X2), a__div#(s X, s Y) -> a__geq#(X, Y)) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# geq(X1, X2) -> a__geq#(X1, X2)) (mark# s X -> mark# X, mark# minus(X1, X2) -> a__minus#(X1, X2)) (mark# s X -> mark# X, mark# div(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2)) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# if(X1, X2, X3) -> mark# X1, mark# geq(X1, X2) -> a__geq#(X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# minus(X1, X2) -> a__minus#(X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# div(X1, X2) -> mark# X1) (mark# if(X1, X2, X3) -> mark# X1, mark# div(X1, X2) -> a__div#(mark X1, X2)) (mark# if(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (a__geq#(s X, s Y) -> a__geq#(X, Y), a__geq#(s X, s Y) -> a__geq#(X, Y)) (a__div#(s X, s Y) -> a__geq#(X, Y), a__geq#(s X, s Y) -> a__geq#(X, Y)) (a__minus#(s X, s Y) -> a__minus#(X, Y), a__minus#(s X, s Y) -> a__minus#(X, Y)) (mark# div(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# div(X1, X2) -> mark# X1, mark# div(X1, X2) -> a__div#(mark X1, X2)) (mark# div(X1, X2) -> mark# X1, mark# div(X1, X2) -> mark# X1) (mark# div(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(X1, X2)) (mark# div(X1, X2) -> mark# X1, mark# geq(X1, X2) -> a__geq#(X1, X2)) (mark# div(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (mark# div(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# s X -> mark# X) (a__if#(true(), X, Y) -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# div(X1, X2) -> mark# X1) (a__if#(true(), X, Y) -> mark# X, mark# minus(X1, X2) -> a__minus#(X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# geq(X1, X2) -> a__geq#(X1, X2)) (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__if#(true(), X, Y) -> mark# X, mark# if(X1, X2, X3) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X) (a__if#(false(), X, Y) -> mark# Y, mark# div(X1, X2) -> a__div#(mark X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# div(X1, X2) -> mark# X1) (a__if#(false(), X, Y) -> mark# Y, mark# minus(X1, X2) -> a__minus#(X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# geq(X1, X2) -> a__geq#(X1, X2)) (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3)) (a__if#(false(), X, Y) -> mark# Y, mark# if(X1, X2, X3) -> mark# X1) (mark# minus(X1, X2) -> a__minus#(X1, X2), a__minus#(s X, s Y) -> a__minus#(X, Y)) (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(true(), X, Y) -> mark# X) (mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), a__if#(false(), X, Y) -> mark# Y)} STATUS: arrows: 0.727811 SCCS (3): Scc: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2), mark# div(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), mark# if(X1, X2, X3) -> mark# X1} Scc: {a__minus#(s X, s Y) -> a__minus#(X, Y)} Scc: {a__geq#(s X, s Y) -> a__geq#(X, Y)} SCC (8): Strict: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2), mark# div(X1, X2) -> mark# X1, mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3), mark# if(X1, X2, X3) -> mark# X1} Weak: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = 0, [if](x0, x1, x2) = x0 + x1 + x2 + 1, [a__minus](x0, x1) = 0, [a__geq](x0, x1) = 0, [a__div](x0, x1) = 0, [div](x0, x1) = x0, [minus](x0, x1) = 0, [geq](x0, x1) = 0, [s](x0) = x0, [mark](x0) = 0, [0] = 0, [true] = 0, [false] = 0, [a__if#](x0, x1, x2) = x0 + x1, [a__div#](x0, x1) = 0, [mark#](x0) = x0 Strict: mark# if(X1, X2, X3) -> mark# X1 1 + 1X1 + 1X2 + 1X3 >= 0 + 1X1 mark# if(X1, X2, X3) -> a__if#(mark X1, X2, X3) 1 + 1X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 mark# div(X1, X2) -> mark# X1 0 + 1X1 + 0X2 >= 0 + 1X1 mark# div(X1, X2) -> a__div#(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 mark# s X -> mark# X 0 + 1X >= 0 + 1X a__if#(false(), X, Y) -> mark# Y 0 + 1Y + 1X >= 0 + 1Y a__if#(true(), X, Y) -> mark# X 0 + 1Y + 1X >= 0 + 1X a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 0 + 0Y + 0X >= 0 + 0Y + 0X Weak: mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 mark geq(X1, X2) -> a__geq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark minus(X1, X2) -> a__minus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark div(X1, X2) -> a__div(mark X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark false() -> false() 0 >= 0 mark true() -> true() 0 >= 0 mark s X -> s mark X 0 + 0X >= 0 + 0X mark 0() -> 0() 0 >= 0 a__if(false(), X, Y) -> mark Y 0 + 0Y + 0X >= 0 + 0Y a__if(true(), X, Y) -> mark X 0 + 0Y + 0X >= 0 + 0X a__if(X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 1X2 + 1X3 a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 0 + 0Y + 0X >= 0 + 0Y + 0X a__div(0(), s Y) -> 0() 0 + 0Y >= 0 a__div(X1, X2) -> div(X1, X2) 0 + 0X1 + 0X2 >= 0 + 1X1 + 0X2 a__geq(s X, s Y) -> a__geq(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X a__geq(0(), s Y) -> false() 0 + 0Y >= 0 a__geq(X1, X2) -> geq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 a__geq(X, 0()) -> true() 0 + 0X >= 0 a__minus(s X, s Y) -> a__minus(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X a__minus(0(), Y) -> 0() 0 + 0Y >= 0 a__minus(X1, X2) -> minus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2), mark# div(X1, X2) -> mark# X1} SCC (6): Strict: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2), mark# div(X1, X2) -> mark# X1} Weak: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + x1 + 1, [if](x0, x1, x2) = 0, [a__minus](x0, x1) = 0, [a__geq](x0, x1) = 0, [a__div](x0, x1) = 0, [div](x0, x1) = x0 + 1, [minus](x0, x1) = 0, [geq](x0, x1) = 0, [s](x0) = x0, [mark](x0) = 0, [0] = 0, [true] = 0, [false] = 1, [a__if#](x0, x1, x2) = x0 + x1, [a__div#](x0, x1) = 1, [mark#](x0) = x0 Strict: mark# div(X1, X2) -> mark# X1 1 + 1X1 + 0X2 >= 0 + 1X1 mark# div(X1, X2) -> a__div#(mark X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 0X2 mark# s X -> mark# X 0 + 1X >= 0 + 1X a__if#(false(), X, Y) -> mark# Y 0 + 1Y + 1X >= 0 + 1Y a__if#(true(), X, Y) -> mark# X 0 + 1Y + 1X >= 0 + 1X a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 1 + 0Y + 0X >= 1 + 0Y + 0X Weak: mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 0 + 0X1 + 0X2 + 0X3 >= 1 + 0X1 + 1X2 + 0X3 mark geq(X1, X2) -> a__geq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark minus(X1, X2) -> a__minus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark div(X1, X2) -> a__div(mark X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark false() -> false() 0 >= 1 mark true() -> true() 0 >= 0 mark s X -> s mark X 0 + 0X >= 0 + 0X mark 0() -> 0() 0 >= 0 a__if(false(), X, Y) -> mark Y 2 + 0Y + 1X >= 0 + 0Y a__if(true(), X, Y) -> mark X 1 + 0Y + 1X >= 0 + 0X a__if(X1, X2, X3) -> if(X1, X2, X3) 1 + 1X1 + 1X2 + 0X3 >= 0 + 0X1 + 0X2 + 0X3 a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 0 + 0Y + 0X >= 2 + 0Y + 0X a__div(0(), s Y) -> 0() 0 + 0Y >= 0 a__div(X1, X2) -> div(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 a__geq(s X, s Y) -> a__geq(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X a__geq(0(), s Y) -> false() 0 + 0Y >= 1 a__geq(X1, X2) -> geq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 a__geq(X, 0()) -> true() 0 + 0X >= 0 a__minus(s X, s Y) -> a__minus(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X a__minus(0(), Y) -> 0() 0 + 0Y >= 0 a__minus(X1, X2) -> minus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2)} SCC (5): Strict: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# s X -> mark# X, mark# div(X1, X2) -> a__div#(mark X1, X2)} Weak: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + x1, [if](x0, x1, x2) = x0 + x1, [a__minus](x0, x1) = 0, [a__geq](x0, x1) = 0, [a__div](x0, x1) = x0, [div](x0, x1) = x0, [minus](x0, x1) = 0, [geq](x0, x1) = 0, [s](x0) = x0 + 1, [mark](x0) = x0, [0] = 0, [true] = 0, [false] = 0, [a__if#](x0, x1, x2) = x0 + x1, [a__div#](x0, x1) = x0, [mark#](x0) = x0 Strict: mark# div(X1, X2) -> a__div#(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 mark# s X -> mark# X 1 + 1X >= 0 + 1X a__if#(false(), X, Y) -> mark# Y 0 + 1Y + 1X >= 0 + 1Y a__if#(true(), X, Y) -> mark# X 0 + 1Y + 1X >= 0 + 1X a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 1 + 0Y + 1X >= 1 + 0Y + 0X Weak: mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 mark geq(X1, X2) -> a__geq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark minus(X1, X2) -> a__minus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 mark div(X1, X2) -> a__div(mark X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 mark false() -> false() 0 >= 0 mark true() -> true() 0 >= 0 mark s X -> s mark X 1 + 1X >= 1 + 1X mark 0() -> 0() 0 >= 0 a__if(false(), X, Y) -> mark Y 0 + 1Y + 1X >= 0 + 1Y a__if(true(), X, Y) -> mark X 0 + 1Y + 1X >= 0 + 1X a__if(X1, X2, X3) -> if(X1, X2, X3) 0 + 0X1 + 1X2 + 1X3 >= 0 + 0X1 + 1X2 + 1X3 a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 1 + 0Y + 1X >= 1 + 0Y + 0X a__div(0(), s Y) -> 0() 0 + 0Y >= 0 a__div(X1, X2) -> div(X1, X2) 0 + 1X1 + 0X2 >= 0 + 1X1 + 0X2 a__geq(s X, s Y) -> a__geq(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X a__geq(0(), s Y) -> false() 0 + 0Y >= 0 a__geq(X1, X2) -> geq(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 a__geq(X, 0()) -> true() 0 + 0X >= 0 a__minus(s X, s Y) -> a__minus(X, Y) 0 + 0Y + 0X >= 0 + 0Y + 0X a__minus(0(), Y) -> 0() 0 + 0Y >= 0 a__minus(X1, X2) -> minus(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# div(X1, X2) -> a__div#(mark X1, X2)} SCC (4): Strict: { a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if#(true(), X, Y) -> mark# X, a__if#(false(), X, Y) -> mark# Y, mark# div(X1, X2) -> a__div#(mark X1, X2)} Weak: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + x1 + 1, [if](x0, x1, x2) = x0 + x1 + 1, [a__minus](x0, x1) = 1, [a__geq](x0, x1) = 1, [a__div](x0, x1) = x0 + 1, [div](x0, x1) = x0 + 1, [minus](x0, x1) = 1, [geq](x0, x1) = 1, [s](x0) = 1, [mark](x0) = x0, [0] = 0, [true] = 1, [false] = 1, [a__if#](x0, x1, x2) = x0 + x1 + x2, [a__div#](x0, x1) = x0 + 1, [mark#](x0) = x0 + 1 Strict: mark# div(X1, X2) -> a__div#(mark X1, X2) 2 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 a__if#(false(), X, Y) -> mark# Y 1 + 1Y + 1X >= 1 + 1Y a__if#(true(), X, Y) -> mark# X 1 + 1Y + 1X >= 1 + 1X a__div#(s X, s Y) -> a__if#(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 2 + 0Y + 0X >= 2 + 0Y + 0X Weak: mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 1 + 0X1 + 1X2 + 1X3 >= 1 + 0X1 + 1X2 + 1X3 mark geq(X1, X2) -> a__geq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark minus(X1, X2) -> a__minus(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 mark div(X1, X2) -> a__div(mark X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 mark false() -> false() 1 >= 1 mark true() -> true() 1 >= 1 mark s X -> s mark X 1 + 0X >= 1 + 0X mark 0() -> 0() 0 >= 0 a__if(false(), X, Y) -> mark Y 1 + 1Y + 1X >= 0 + 1Y a__if(true(), X, Y) -> mark X 1 + 1Y + 1X >= 0 + 1X a__if(X1, X2, X3) -> if(X1, X2, X3) 1 + 0X1 + 1X2 + 1X3 >= 1 + 0X1 + 1X2 + 1X3 a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 2 + 0Y + 0X >= 2 + 0Y + 0X a__div(0(), s Y) -> 0() 1 + 0Y >= 0 a__div(X1, X2) -> div(X1, X2) 1 + 1X1 + 0X2 >= 1 + 1X1 + 0X2 a__geq(s X, s Y) -> a__geq(X, Y) 1 + 0Y + 0X >= 1 + 0Y + 0X a__geq(0(), s Y) -> false() 1 + 0Y >= 1 a__geq(X1, X2) -> geq(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 a__geq(X, 0()) -> true() 1 + 0X >= 1 a__minus(s X, s Y) -> a__minus(X, Y) 1 + 0Y + 0X >= 1 + 0Y + 0X a__minus(0(), Y) -> 0() 1 + 0Y >= 0 a__minus(X1, X2) -> minus(X1, X2) 1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 SCCS (0): SCC (1): Strict: {a__minus#(s X, s Y) -> a__minus#(X, Y)} Weak: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + x1 + x2, [if](x0, x1, x2) = 1, [a__minus](x0, x1) = x0 + 1, [a__geq](x0, x1) = x0 + 1, [a__div](x0, x1) = x0 + 1, [div](x0, x1) = 1, [minus](x0, x1) = 1, [geq](x0, x1) = 1, [s](x0) = x0 + 1, [mark](x0) = x0 + 1, [0] = 1, [true] = 0, [false] = 0, [a__minus#](x0, x1) = x0 + 1 Strict: a__minus#(s X, s Y) -> a__minus#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 1X2 + 1X3 mark geq(X1, X2) -> a__geq(X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 mark minus(X1, X2) -> a__minus(X1, X2) 2 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 mark div(X1, X2) -> a__div(mark X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 mark false() -> false() 1 >= 0 mark true() -> true() 1 >= 0 mark s X -> s mark X 2 + 1X >= 2 + 1X mark 0() -> 0() 2 >= 1 a__if(false(), X, Y) -> mark Y 0 + 1Y + 1X >= 1 + 1Y a__if(true(), X, Y) -> mark X 0 + 1Y + 1X >= 1 + 1X a__if(X1, X2, X3) -> if(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 1 + 0X1 + 0X2 + 0X3 a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 2 + 1Y + 0X >= 4 + 1Y + 0X a__div(0(), s Y) -> 0() 2 + 1Y >= 1 a__div(X1, X2) -> div(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 0X2 a__geq(s X, s Y) -> a__geq(X, Y) 2 + 1Y + 0X >= 1 + 1Y + 0X a__geq(0(), s Y) -> false() 2 + 1Y >= 0 a__geq(X1, X2) -> geq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 0X2 a__geq(X, 0()) -> true() 2 + 0X >= 0 a__minus(s X, s Y) -> a__minus(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X a__minus(0(), Y) -> 0() 2 + 0Y >= 1 a__minus(X1, X2) -> minus(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 0X2 Qed SCC (1): Strict: {a__geq#(s X, s Y) -> a__geq#(X, Y)} Weak: { a__minus(X1, X2) -> minus(X1, X2), a__minus(0(), Y) -> 0(), a__minus(s X, s Y) -> a__minus(X, Y), a__geq(X, 0()) -> true(), a__geq(X1, X2) -> geq(X1, X2), a__geq(0(), s Y) -> false(), a__geq(s X, s Y) -> a__geq(X, Y), a__div(X1, X2) -> div(X1, X2), a__div(0(), s Y) -> 0(), a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()), a__if(X1, X2, X3) -> if(X1, X2, X3), a__if(true(), X, Y) -> mark X, a__if(false(), X, Y) -> mark Y, mark 0() -> 0(), mark s X -> s mark X, mark true() -> true(), mark false() -> false(), mark div(X1, X2) -> a__div(mark X1, X2), mark minus(X1, X2) -> a__minus(X1, X2), mark geq(X1, X2) -> a__geq(X1, X2), mark if(X1, X2, X3) -> a__if(mark X1, X2, X3)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [a__if](x0, x1, x2) = x0 + x1 + x2, [if](x0, x1, x2) = 1, [a__minus](x0, x1) = x0 + 1, [a__geq](x0, x1) = x0 + 1, [a__div](x0, x1) = x0 + 1, [div](x0, x1) = 1, [minus](x0, x1) = 1, [geq](x0, x1) = 1, [s](x0) = x0 + 1, [mark](x0) = x0 + 1, [0] = 1, [true] = 0, [false] = 0, [a__geq#](x0, x1) = x0 + 1 Strict: a__geq#(s X, s Y) -> a__geq#(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X Weak: mark if(X1, X2, X3) -> a__if(mark X1, X2, X3) 2 + 0X1 + 0X2 + 0X3 >= 1 + 1X1 + 1X2 + 1X3 mark geq(X1, X2) -> a__geq(X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 mark minus(X1, X2) -> a__minus(X1, X2) 2 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 mark div(X1, X2) -> a__div(mark X1, X2) 2 + 0X1 + 0X2 >= 1 + 0X1 + 1X2 mark false() -> false() 1 >= 0 mark true() -> true() 1 >= 0 mark s X -> s mark X 2 + 1X >= 2 + 1X mark 0() -> 0() 2 >= 1 a__if(false(), X, Y) -> mark Y 0 + 1Y + 1X >= 1 + 1Y a__if(true(), X, Y) -> mark X 0 + 1Y + 1X >= 1 + 1X a__if(X1, X2, X3) -> if(X1, X2, X3) 0 + 1X1 + 1X2 + 1X3 >= 1 + 0X1 + 0X2 + 0X3 a__div(s X, s Y) -> a__if(a__geq(X, Y), s div(minus(X, Y), s Y), 0()) 2 + 1Y + 0X >= 4 + 1Y + 0X a__div(0(), s Y) -> 0() 2 + 1Y >= 1 a__div(X1, X2) -> div(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 0X2 a__geq(s X, s Y) -> a__geq(X, Y) 2 + 1Y + 0X >= 1 + 1Y + 0X a__geq(0(), s Y) -> false() 2 + 1Y >= 0 a__geq(X1, X2) -> geq(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 0X2 a__geq(X, 0()) -> true() 2 + 0X >= 0 a__minus(s X, s Y) -> a__minus(X, Y) 2 + 0Y + 1X >= 1 + 0Y + 1X a__minus(0(), Y) -> 0() 2 + 0Y >= 1 a__minus(X1, X2) -> minus(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 0X2 Qed