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) Matrix Interpretation Processor: dim=1 interpretation: [mark#](x0) = 3x0 + 1, [a__if#](x0, x1, x2) = x0 + 3x1 + 4x2 + 1, [a__div#](x0, x1) = 7x0 + 7, [if](x0, x1, x2) = x0 + 3x1 + 7x2, [geq](x0, x1) = 0, [mark](x0) = x0, [a__if](x0, x1, x2) = x0 + 3x1 + 7x2, [div](x0, x1) = 7x0 + 6, [minus](x0, x1) = 0, [a__div](x0, x1) = 7x0 + 6, [false] = 0, [true] = 0, [a__geq](x0, x1) = 0, [s](x0) = x0 + 3, [a__minus](x0, x1) = 0, [0] = 0 orientation: mark#(if(X1,X2,X3)) = 3X1 + 9X2 + 21X3 + 1 >= 3X1 + 1 = mark#(X1) mark#(div(X1,X2)) = 21X1 + 19 >= 7X1 + 7 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 7X + 28 >= 28 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = 3X + 4Y + 1 >= 3X + 1 = mark#(X) mark#(if(X1,X2,X3)) = 3X1 + 9X2 + 21X3 + 1 >= X1 + 3X2 + 4X3 + 1 = a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) = 3X + 4Y + 1 >= 3Y + 1 = mark#(Y) mark#(s(X)) = 3X + 10 >= 3X + 1 = mark#(X) a__minus(0(),Y) = 0 >= 0 = 0() a__minus(s(X),s(Y)) = 0 >= 0 = 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)) = 7X + 27 >= 27 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = 3X + 7Y >= X = mark(X) a__if(false(),X,Y) = 3X + 7Y >= Y = mark(Y) mark(minus(X1,X2)) = 0 >= 0 = a__minus(X1,X2) mark(geq(X1,X2)) = 0 >= 0 = a__geq(X1,X2) mark(div(X1,X2)) = 7X1 + 6 >= 7X1 + 6 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X1 + 3X2 + 7X3 >= X1 + 3X2 + 7X3 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X + 3 >= X + 3 = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__minus(X1,X2) = 0 >= 0 = minus(X1,X2) a__geq(X1,X2) = 0 >= 0 = geq(X1,X2) a__div(X1,X2) = 7X1 + 6 >= 7X1 + 6 = div(X1,X2) a__if(X1,X2,X3) = X1 + 3X2 + 7X3 >= X1 + 3X2 + 7X3 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> mark#(X1) 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) 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: 1 #rules: 4 #arcs: 30/25 DPs: mark#(if(X1,X2,X3)) -> mark#(X1) mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) a__if#(true(),X,Y) -> mark#(X) a__if#(false(),X,Y) -> mark#(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) Arctic Interpretation Processor: dimension: 1 interpretation: [mark#](x0) = 4x0, [a__if#](x0, x1, x2) = 4x1 + 6x2, [if](x0, x1, x2) = 2x0 + 3x1 + 2x2 + 0, [geq](x0, x1) = 1, [mark](x0) = 2x0, [a__if](x0, x1, x2) = 2x0 + 4x1 + 4x2 + 0, [div](x0, x1) = 2x0 + 3x1, [minus](x0, x1) = 0, [a__div](x0, x1) = 2x0 + 4x1, [false] = 0, [true] = 2, [a__geq](x0, x1) = 2, [s](x0) = 0, [a__minus](x0, x1) = 2, [0] = 0 orientation: mark#(if(X1,X2,X3)) = 6X1 + 7X2 + 6X3 + 4 >= 4X1 = mark#(X1) mark#(if(X1,X2,X3)) = 6X1 + 7X2 + 6X3 + 4 >= 4X2 + 6X3 = a__if#(mark(X1),X2,X3) a__if#(true(),X,Y) = 4X + 6Y >= 4X = mark#(X) a__if#(false(),X,Y) = 4X + 6Y >= 4Y = mark#(Y) a__minus(0(),Y) = 2 >= 0 = 0() a__minus(s(X),s(Y)) = 2 >= 2 = a__minus(X,Y) a__geq(X,0()) = 2 >= 2 = true() a__geq(0(),s(Y)) = 2 >= 0 = false() a__geq(s(X),s(Y)) = 2 >= 2 = a__geq(X,Y) a__div(0(),s(Y)) = 4 >= 0 = 0() a__div(s(X),s(Y)) = 4 >= 4 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = 4X + 4Y + 4 >= 2X = mark(X) a__if(false(),X,Y) = 4X + 4Y + 2 >= 2Y = mark(Y) mark(minus(X1,X2)) = 2 >= 2 = a__minus(X1,X2) mark(geq(X1,X2)) = 3 >= 2 = a__geq(X1,X2) mark(div(X1,X2)) = 4X1 + 5X2 >= 4X1 + 4X2 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = 4X1 + 5X2 + 4X3 + 2 >= 4X1 + 4X2 + 4X3 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 2 >= 0 = 0() mark(s(X)) = 2 >= 0 = s(mark(X)) mark(true()) = 4 >= 2 = true() mark(false()) = 2 >= 0 = false() a__minus(X1,X2) = 2 >= 0 = minus(X1,X2) a__geq(X1,X2) = 2 >= 1 = geq(X1,X2) a__div(X1,X2) = 2X1 + 4X2 >= 2X1 + 3X2 = div(X1,X2) a__if(X1,X2,X3) = 2X1 + 4X2 + 4X3 + 0 >= 2X1 + 3X2 + 2X3 + 0 = if(X1,X2,X3) problem: DPs: mark#(if(X1,X2,X3)) -> a__if#(mark(X1),X2,X3) 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) Subterm Criterion Processor: simple projection: pi(a__if#) = 1 pi(mark#) = 0 problem: DPs: 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: 8/1 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