YES Problem: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Proof: DP Processor: DPs: 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#(minus(X1,X2)) -> a__minus#(X1,X2) mark#(geq(X1,X2)) -> a__geq#(X1,X2) mark#(div(X1,X2)) -> mark#(X1) mark#(div(X1,X2)) -> a__div#(mark(X1),X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) TDG Processor: DPs: 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#(minus(X1,X2)) -> a__minus#(X1,X2) mark#(geq(X1,X2)) -> a__geq#(X1,X2) mark#(div(X1,X2)) -> mark#(X1) mark#(div(X1,X2)) -> a__div#(mark(X1),X2) mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) graph: mark#(if(X1,X2,X3)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) 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#(if(X1,X2,X3)) -> 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#(div(X1,X2)) -> mark#(X1) 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)) -> a__if#(mark(X1),X2,X3) -> a__if#(false(),X,Y) -> mark#(Y) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) -> 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)) -> mark#(X1) -> mark#(s(X)) -> mark#(X) 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) 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#(geq(X1,X2)) -> a__geq#(X1,X2) mark#(div(X1,X2)) -> mark#(X1) -> mark#(minus(X1,X2)) -> a__minus#(X1,X2) 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#(minus(X1,X2)) -> a__minus#(X1,X2) -> a__minus#(s(X),s(Y)) -> a__minus#(X,Y) mark#(s(X)) -> mark#(X) -> mark#(s(X)) -> mark#(X) mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(s(X)) -> mark#(X) -> mark#(if(X1,X2,X3)) -> mark#(X1) mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> a__div#(mark(X1),X2) mark#(s(X)) -> mark#(X) -> mark#(div(X1,X2)) -> mark#(X1) 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) a__if#(false(),X,Y) -> mark#(Y) -> mark#(s(X)) -> mark#(X) 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) 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#(geq(X1,X2)) -> a__geq#(X1,X2) a__if#(false(),X,Y) -> mark#(Y) -> mark#(minus(X1,X2)) -> a__minus#(X1,X2) a__if#(true(),X,Y) -> mark#(X) -> mark#(s(X)) -> mark#(X) 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#(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#(geq(X1,X2)) -> a__geq#(X1,X2) a__if#(true(),X,Y) -> mark#(X) -> mark#(minus(X1,X2)) -> a__minus#(X1,X2) 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) a__div#(s(X),s(Y)) -> a__geq#(X,Y) -> a__geq#(s(X),s(Y)) -> a__geq#(X,Y) a__geq#(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) SCC Processor: #sccs: 3 #rules: 10 #arcs: 46/169 DPs: mark#(if(X1,X2,X3)) -> mark#(X1) mark#(div(X1,X2)) -> mark#(X1) 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()) 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) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__if#](x0, x1, x2) = x0 + x1 + x2 + 0, [a__div#](x0, x1) = 5x0 + 4x1 + 1, [if](x0, x1, x2) = x0 + x1 + 1x2 + 0, [geq](x0, x1) = 0, [mark](x0) = x0, [a__if](x0, x1, x2) = x0 + x1 + 1x2 + 0, [div](x0, x1) = 5x0 + 4x1 + 1, [minus](x0, x1) = x0, [a__div](x0, x1) = 5x0 + 4x1 + 1, [false] = 0, [true] = 0, [a__geq](x0, x1) = 0, [s](x0) = x0, [a__minus](x0, x1) = x0, [0] = 0 orientation: mark#(if(X1,X2,X3)) = X1 + X2 + 1X3 + 0 >= X1 = mark#(X1) mark#(div(X1,X2)) = 5X1 + 4X2 + 1 >= X1 = mark#(X1) mark#(div(X1,X2)) = 5X1 + 4X2 + 1 >= 5X1 + 4X2 + 1 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 5X + 4Y + 1 >= 5X + 4Y + 1 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + Y + 0 >= X = mark#(X) mark#(if(X1,X2,X3)) = X1 + X2 + 1X3 + 0 >= X1 + X2 + X3 + 0 = a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) = X + Y + 0 >= Y = mark#(Y) mark#(s(X)) = X >= X = mark#(X) a__minus(0(),Y) = 0 >= 0 = 0() a__minus(s(X),s(Y)) = X >= X = a__minus(X,Y) a__geq(X,0()) = 0 >= 0 = true() a__geq(0(),s(Y)) = 0 >= 0 = false() a__geq(s(X),s(Y)) = 0 >= 0 = a__geq(X,Y) a__div(0(),s(Y)) = 4Y + 5 >= 0 = 0() a__div(s(X),s(Y)) = 5X + 4Y + 1 >= 5X + 4Y + 1 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 1Y + 0 >= X = mark(X) a__if(false(),X,Y) = X + 1Y + 0 >= Y = mark(Y) mark(minus(X1,X2)) = X1 >= X1 = a__minus(X1,X2) mark(geq(X1,X2)) = 0 >= 0 = a__geq(X1,X2) mark(div(X1,X2)) = 5X1 + 4X2 + 1 >= 5X1 + 4X2 + 1 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X1 + X2 + 1X3 + 0 >= X1 + X2 + 1X3 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X >= X = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__minus(X1,X2) = X1 >= X1 = minus(X1,X2) a__geq(X1,X2) = 0 >= 0 = geq(X1,X2) a__div(X1,X2) = 5X1 + 4X2 + 1 >= 5X1 + 4X2 + 1 = div(X1,X2) a__if(X1,X2,X3) = X1 + X2 + 1X3 + 0 >= X1 + X2 + 1X3 + 0 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X1) 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()) 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) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 6, [a__if#](x0, x1, x2) = x0 + x1 + 4x2 + 6, [a__div#](x0, x1) = 5x0 + 2x1, [if](x0, x1, x2) = x0 + x1 + 4x2, [geq](x0, x1) = 5x0 + 2x1, [mark](x0) = x0, [a__if](x0, x1, x2) = x0 + x1 + 4x2, [div](x0, x1) = 5x0 + 2x1 + 0, [minus](x0, x1) = x0, [a__div](x0, x1) = 5x0 + 2x1 + 0, [false] = 7, [true] = 4, [a__geq](x0, x1) = 5x0 + 2x1, [s](x0) = x0 + 1, [a__minus](x0, x1) = x0, [0] = 2 orientation: mark#(if(X1,X2,X3)) = X1 + X2 + 4X3 + 6 >= X1 + 6 = mark#(X1) mark#(div(X1,X2)) = 5X1 + 2X2 + 6 >= 5X1 + 2X2 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 5X + 2Y + 6 >= 5X + 2Y + 6 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + 4Y + 6 >= X + 6 = mark#(X) mark#(if(X1,X2,X3)) = X1 + X2 + 4X3 + 6 >= X1 + X2 + 4X3 + 6 = a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) = X + 4Y + 7 >= Y + 6 = mark#(Y) mark#(s(X)) = X + 6 >= X + 6 = mark#(X) a__minus(0(),Y) = 2 >= 2 = 0() a__minus(s(X),s(Y)) = X + 1 >= X = a__minus(X,Y) a__geq(X,0()) = 5X + 4 >= 4 = true() a__geq(0(),s(Y)) = 2Y + 7 >= 7 = false() a__geq(s(X),s(Y)) = 5X + 2Y + 6 >= 5X + 2Y = a__geq(X,Y) a__div(0(),s(Y)) = 2Y + 7 >= 2 = 0() a__div(s(X),s(Y)) = 5X + 2Y + 6 >= 5X + 2Y + 6 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 4Y + 4 >= X = mark(X) a__if(false(),X,Y) = X + 4Y + 7 >= Y = mark(Y) mark(minus(X1,X2)) = X1 >= X1 = a__minus(X1,X2) mark(geq(X1,X2)) = 5X1 + 2X2 >= 5X1 + 2X2 = a__geq(X1,X2) mark(div(X1,X2)) = 5X1 + 2X2 + 0 >= 5X1 + 2X2 + 0 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X1 + X2 + 4X3 >= X1 + X2 + 4X3 = a__if(mark(X1),X2,X3) mark(0()) = 2 >= 2 = 0() mark(s(X)) = X + 1 >= X + 1 = s(mark(X)) mark(true()) = 4 >= 4 = true() mark(false()) = 7 >= 7 = false() a__minus(X1,X2) = X1 >= X1 = minus(X1,X2) a__geq(X1,X2) = 5X1 + 2X2 >= 5X1 + 2X2 = geq(X1,X2) a__div(X1,X2) = 5X1 + 2X2 + 0 >= 5X1 + 2X2 + 0 = div(X1,X2) a__if(X1,X2,X3) = X1 + X2 + 4X3 >= X1 + X2 + 4X3 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X1) 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()) a__if#(true(),X,Y) -> mark#(X) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__if#](x0, x1, x2) = x1, [a__div#](x0, x1) = x1 + 5, [if](x0, x1, x2) = x0 + 2x1 + 5x2 + 0, [geq](x0, x1) = x1 + 0, [mark](x0) = 2x0, [a__if](x0, x1, x2) = x0 + 2x1 + 7x2 + 0, [div](x0, x1) = x1 + 5, [minus](x0, x1) = 2x0 + x1 + 2, [a__div](x0, x1) = 2x1 + 7, [false] = 0, [true] = 0, [a__geq](x0, x1) = x1 + 0, [s](x0) = x0, [a__minus](x0, x1) = 2x0 + x1 + 4, [0] = 0 orientation: mark#(if(X1,X2,X3)) = X1 + 2X2 + 5X3 + 0 >= X1 = mark#(X1) mark#(div(X1,X2)) = X2 + 5 >= X2 + 5 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = Y + 5 >= Y + 5 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X >= X = mark#(X) mark#(if(X1,X2,X3)) = X1 + 2X2 + 5X3 + 0 >= X2 = a__if#(mark(X1),X2,X3) mark#(s(X)) = X >= X = mark#(X) a__minus(0(),Y) = Y + 4 >= 0 = 0() a__minus(s(X),s(Y)) = 2X + Y + 4 >= 2X + Y + 4 = a__minus(X,Y) a__geq(X,0()) = 0 >= 0 = true() a__geq(0(),s(Y)) = Y + 0 >= 0 = false() a__geq(s(X),s(Y)) = Y + 0 >= Y + 0 = a__geq(X,Y) a__div(0(),s(Y)) = 2Y + 7 >= 0 = 0() a__div(s(X),s(Y)) = 2Y + 7 >= 2Y + 7 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = 2X + 7Y + 0 >= 2X = mark(X) a__if(false(),X,Y) = 2X + 7Y + 0 >= 2Y = mark(Y) mark(minus(X1,X2)) = 4X1 + 2X2 + 4 >= 2X1 + X2 + 4 = a__minus(X1,X2) mark(geq(X1,X2)) = 2X2 + 2 >= X2 + 0 = a__geq(X1,X2) mark(div(X1,X2)) = 2X2 + 7 >= 2X2 + 7 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = 2X1 + 4X2 + 7X3 + 2 >= 2X1 + 2X2 + 7X3 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 2 >= 0 = 0() mark(s(X)) = 2X >= 2X = s(mark(X)) mark(true()) = 2 >= 0 = true() mark(false()) = 2 >= 0 = false() a__minus(X1,X2) = 2X1 + X2 + 4 >= 2X1 + X2 + 2 = minus(X1,X2) a__geq(X1,X2) = X2 + 0 >= X2 + 0 = geq(X1,X2) a__div(X1,X2) = 2X2 + 7 >= X2 + 5 = div(X1,X2) a__if(X1,X2,X3) = X1 + 2X2 + 7X3 + 0 >= X1 + 2X2 + 5X3 + 0 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X1) 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()) a__if#(true(),X,Y) -> mark#(X) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__if#](x0, x1, x2) = x0 + x1 + 1x2 + 0, [a__div#](x0, x1) = 6x1, [if](x0, x1, x2) = 2x0 + x1 + 5x2 + 3, [geq](x0, x1) = 1x1, [mark](x0) = x0 + 0, [a__if](x0, x1, x2) = 2x0 + x1 + 5x2 + 3, [div](x0, x1) = 6x1, [minus](x0, x1) = 4x0 + 3x1, [a__div](x0, x1) = 6x1, [false] = 2, [true] = 0, [a__geq](x0, x1) = 1x1 + 0, [s](x0) = x0 + 1, [a__minus](x0, x1) = 4x0 + 3x1, [0] = 0 orientation: mark#(if(X1,X2,X3)) = 2X1 + X2 + 5X3 + 3 >= X1 = mark#(X1) mark#(div(X1,X2)) = 6X2 >= 6X2 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 6Y + 7 >= 6Y + 7 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + 1Y + 0 >= X = mark#(X) mark#(s(X)) = X + 1 >= X = mark#(X) a__minus(0(),Y) = 3Y + 4 >= 0 = 0() a__minus(s(X),s(Y)) = 4X + 3Y + 5 >= 4X + 3Y = a__minus(X,Y) a__geq(X,0()) = 1 >= 0 = true() a__geq(0(),s(Y)) = 1Y + 2 >= 2 = false() a__geq(s(X),s(Y)) = 1Y + 2 >= 1Y + 0 = a__geq(X,Y) a__div(0(),s(Y)) = 6Y + 7 >= 0 = 0() a__div(s(X),s(Y)) = 6Y + 7 >= 6Y + 7 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 5Y + 3 >= X + 0 = mark(X) a__if(false(),X,Y) = X + 5Y + 4 >= Y + 0 = mark(Y) mark(minus(X1,X2)) = 4X1 + 3X2 + 0 >= 4X1 + 3X2 = a__minus(X1,X2) mark(geq(X1,X2)) = 1X2 + 0 >= 1X2 + 0 = a__geq(X1,X2) mark(div(X1,X2)) = 6X2 + 0 >= 6X2 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = 2X1 + X2 + 5X3 + 3 >= 2X1 + X2 + 5X3 + 3 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X + 1 >= X + 1 = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 2 >= 2 = false() a__minus(X1,X2) = 4X1 + 3X2 >= 4X1 + 3X2 = minus(X1,X2) a__geq(X1,X2) = 1X2 + 0 >= 1X2 = geq(X1,X2) a__div(X1,X2) = 6X2 >= 6X2 = div(X1,X2) a__if(X1,X2,X3) = 2X1 + X2 + 5X3 + 3 >= 2X1 + X2 + 5X3 + 3 = if(X1,X2,X3) problem: DPs: 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()) a__if#(true(),X,Y) -> mark#(X) mark#(s(X)) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0 + 0, [a__if#](x0, x1, x2) = x0 + x1 + x2 + 0, [a__div#](x0, x1) = 2x0 + 0, [if](x0, x1, x2) = x1 + x2, [geq](x0, x1) = x0, [mark](x0) = x0 + 0, [a__if](x0, x1, x2) = x1 + x2 + 0, [div](x0, x1) = 2x0 + 2, [minus](x0, x1) = x0, [a__div](x0, x1) = 2x0 + 2, [false] = 0, [true] = 0, [a__geq](x0, x1) = x0 + 0, [s](x0) = 1x0 + 1, [a__minus](x0, x1) = x0, [0] = 3 orientation: mark#(div(X1,X2)) = 2X1 + 2 >= 2X1 + 2 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 3X + 3 >= 3X + 3 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + Y + 0 >= X + 0 = mark#(X) mark#(s(X)) = 1X + 1 >= X + 0 = mark#(X) a__minus(0(),Y) = 3 >= 3 = 0() a__minus(s(X),s(Y)) = 1X + 1 >= X = a__minus(X,Y) a__geq(X,0()) = X + 0 >= 0 = true() a__geq(0(),s(Y)) = 3 >= 0 = false() a__geq(s(X),s(Y)) = 1X + 1 >= X + 0 = a__geq(X,Y) a__div(0(),s(Y)) = 5 >= 3 = 0() a__div(s(X),s(Y)) = 3X + 3 >= 3X + 3 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + Y + 0 >= X + 0 = mark(X) a__if(false(),X,Y) = X + Y + 0 >= Y + 0 = mark(Y) mark(minus(X1,X2)) = X1 + 0 >= X1 = a__minus(X1,X2) mark(geq(X1,X2)) = X1 + 0 >= X1 + 0 = a__geq(X1,X2) mark(div(X1,X2)) = 2X1 + 2 >= 2X1 + 2 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X2 + X3 + 0 >= X2 + X3 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 3 >= 3 = 0() mark(s(X)) = 1X + 1 >= 1X + 1 = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__minus(X1,X2) = X1 >= X1 = minus(X1,X2) a__geq(X1,X2) = X1 + 0 >= X1 = geq(X1,X2) a__div(X1,X2) = 2X1 + 2 >= 2X1 + 2 = div(X1,X2) a__if(X1,X2,X3) = X2 + X3 + 0 >= X2 + X3 = if(X1,X2,X3) problem: DPs: 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()) a__if#(true(),X,Y) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = x0, [a__if#](x0, x1, x2) = x0 + x1 + x2 + 0, [a__div#](x0, x1) = x1 + 1, [if](x0, x1, x2) = x0 + x1 + 6x2, [geq](x0, x1) = 0, [mark](x0) = x0 + 0, [a__if](x0, x1, x2) = x0 + x1 + 6x2 + 0, [div](x0, x1) = x1 + 6, [minus](x0, x1) = 2, [a__div](x0, x1) = x1 + 6, [false] = 0, [true] = 0, [a__geq](x0, x1) = 0, [s](x0) = 0, [a__minus](x0, x1) = 2, [0] = 0 orientation: mark#(div(X1,X2)) = X2 + 6 >= X2 + 1 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 1 >= 0 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + Y + 0 >= X = mark#(X) a__minus(0(),Y) = 2 >= 0 = 0() a__minus(s(X),s(Y)) = 2 >= 2 = a__minus(X,Y) a__geq(X,0()) = 0 >= 0 = true() a__geq(0(),s(Y)) = 0 >= 0 = false() a__geq(s(X),s(Y)) = 0 >= 0 = a__geq(X,Y) a__div(0(),s(Y)) = 6 >= 0 = 0() a__div(s(X),s(Y)) = 6 >= 6 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 6Y + 0 >= X + 0 = mark(X) a__if(false(),X,Y) = X + 6Y + 0 >= Y + 0 = mark(Y) mark(minus(X1,X2)) = 2 >= 2 = a__minus(X1,X2) mark(geq(X1,X2)) = 0 >= 0 = a__geq(X1,X2) mark(div(X1,X2)) = X2 + 6 >= X2 + 6 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X1 + X2 + 6X3 + 0 >= X1 + X2 + 6X3 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = 0 >= 0 = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__minus(X1,X2) = 2 >= 2 = minus(X1,X2) a__geq(X1,X2) = 0 >= 0 = geq(X1,X2) a__div(X1,X2) = X2 + 6 >= X2 + 6 = div(X1,X2) a__if(X1,X2,X3) = X1 + X2 + 6X3 + 0 >= X1 + X2 + 6X3 = if(X1,X2,X3) problem: DPs: mark#(div(X1,X2)) -> a__div#(mark(X1),X2) a__if#(true(),X,Y) -> mark#(X) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) SCC Processor: #sccs: 0 #rules: 0 #arcs: 30/4 DPs: a__geq#(s(X),s(Y)) -> a__geq#(X,Y) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Subterm Criterion Processor: simple projection: pi(a__geq#) = 1 problem: DPs: TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Qed DPs: a__minus#(s(X),s(Y)) -> a__minus#(X,Y) TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Subterm Criterion Processor: simple projection: pi(a__minus#) = 1 problem: DPs: TRS: a__minus(0(),Y) -> 0() a__minus(s(X),s(Y)) -> a__minus(X,Y) a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) 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(true(),X,Y) -> mark(X) a__if(false(),X,Y) -> mark(Y) mark(minus(X1,X2)) -> a__minus(X1,X2) mark(geq(X1,X2)) -> a__geq(X1,X2) mark(div(X1,X2)) -> a__div(mark(X1),X2) mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3) mark(0()) -> 0() mark(s(X)) -> s(mark(X)) mark(true()) -> true() mark(false()) -> false() a__minus(X1,X2) -> minus(X1,X2) a__geq(X1,X2) -> geq(X1,X2) a__div(X1,X2) -> div(X1,X2) a__if(X1,X2,X3) -> if(X1,X2,X3) Qed