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 usable rules: interpretation: [mark#](x0) = x0, [a__if#](x0, x1, x2) = x1 + x2, [a__div#](x0, x1) = x1, [if](x0, x1, x2) = 1x0 + x1 + x2 + 0, [geq](x0, x1) = x0 + x1 + 7, [mark](x0) = x0 + 0, [a__if](x0, x1, x2) = 1x0 + x1 + 1x2 + 0, [div](x0, x1) = x0 + x1 + 0, [minus](x0, x1) = x1, [a__div](x0, x1) = x1 + 0, [false] = 3, [true] = 2, [a__geq](x0, x1) = 2x0 + x1 + 0, [s](x0) = x0 + 0, [a__minus](x0, x1) = 4x0 + 0, [0] = 0 orientation: mark#(if(X1,X2,X3)) = 1X1 + X2 + X3 + 0 >= X1 = mark#(X1) mark#(div(X1,X2)) = X1 + X2 + 0 >= X1 = mark#(X1) mark#(div(X1,X2)) = X1 + X2 + 0 >= X2 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = Y + 0 >= Y + 0 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + Y >= X = mark#(X) mark#(if(X1,X2,X3)) = 1X1 + X2 + X3 + 0 >= X2 + X3 = a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) = X + Y >= Y = mark#(Y) mark#(s(X)) = X + 0 >= X = mark#(X) a__minus(0(),Y) = 4 >= 0 = 0() a__minus(s(X),s(Y)) = 4X + 4 >= 4X + 0 = a__minus(X,Y) a__geq(X,0()) = 2X + 0 >= 2 = true() a__geq(0(),s(Y)) = Y + 2 >= 3 = false() a__geq(s(X),s(Y)) = 2X + Y + 2 >= 2X + Y + 0 = a__geq(X,Y) a__div(0(),s(Y)) = Y + 0 >= 0 = 0() a__div(s(X),s(Y)) = Y + 0 >= 3X + 1Y + 1 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 1Y + 3 >= X + 0 = mark(X) a__if(false(),X,Y) = X + 1Y + 4 >= Y + 0 = mark(Y) mark(minus(X1,X2)) = X2 + 0 >= 4X1 + 0 = a__minus(X1,X2) mark(geq(X1,X2)) = X1 + X2 + 7 >= 2X1 + X2 + 0 = a__geq(X1,X2) mark(div(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = 1X1 + X2 + X3 + 0 >= 1X1 + X2 + 1X3 + 1 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X + 0 >= X + 0 = s(mark(X)) mark(true()) = 2 >= 2 = true() mark(false()) = 3 >= 3 = false() a__minus(X1,X2) = 4X1 + 0 >= X2 = minus(X1,X2) a__geq(X1,X2) = 2X1 + X2 + 0 >= X1 + X2 + 7 = geq(X1,X2) a__div(X1,X2) = X2 + 0 >= X1 + X2 + 0 = div(X1,X2) a__if(X1,X2,X3) = 1X1 + X2 + 1X3 + 0 >= 1X1 + X2 + X3 + 0 = if(X1,X2,X3) problem: DPs: 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) Restore Modifier: DPs: 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 usable rules: interpretation: [mark#](x0) = x0 + 1, [a__if#](x0, x1, x2) = x1 + x2 + 1, [a__div#](x0, x1) = 4x1 + 1, [if](x0, x1, x2) = x0 + 4x1 + 2x2 + 2, [geq](x0, x1) = 4x0 + x1 + 0, [mark](x0) = x0, [a__if](x0, x1, x2) = x0 + x1 + 0, [div](x0, x1) = x0 + 4x1, [minus](x0, x1) = x1, [a__div](x0, x1) = x0 + x1 + 0, [false] = 0, [true] = 0, [a__geq](x0, x1) = x0 + x1, [s](x0) = x0 + 0, [a__minus](x0, x1) = x0 + x1 + 0, [0] = 0 orientation: mark#(div(X1,X2)) = X1 + 4X2 + 1 >= X1 + 1 = mark#(X1) mark#(div(X1,X2)) = X1 + 4X2 + 1 >= 4X2 + 1 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 4Y + 4 >= 4Y + 4 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + Y + 1 >= X + 1 = mark#(X) mark#(if(X1,X2,X3)) = X1 + 4X2 + 2X3 + 2 >= X2 + X3 + 1 = a__if#(mark(X1),X2,X3) a__if#(false(),X,Y) = X + Y + 1 >= Y + 1 = mark#(Y) mark#(s(X)) = X + 1 >= X + 1 = mark#(X) a__minus(0(),Y) = Y + 0 >= 0 = 0() a__minus(s(X),s(Y)) = X + Y + 0 >= X + Y + 0 = a__minus(X,Y) a__geq(X,0()) = X + 0 >= 0 = true() a__geq(0(),s(Y)) = Y + 0 >= 0 = false() a__geq(s(X),s(Y)) = X + Y + 0 >= X + Y = a__geq(X,Y) a__div(0(),s(Y)) = Y + 0 >= 0 = 0() a__div(s(X),s(Y)) = X + Y + 0 >= X + 4Y + 4 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 0 >= X = mark(X) a__if(false(),X,Y) = X + 0 >= Y = mark(Y) mark(minus(X1,X2)) = X2 >= X1 + X2 + 0 = a__minus(X1,X2) mark(geq(X1,X2)) = 4X1 + X2 + 0 >= X1 + X2 = a__geq(X1,X2) mark(div(X1,X2)) = X1 + 4X2 >= X1 + X2 + 0 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X1 + 4X2 + 2X3 + 2 >= X1 + X2 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X + 0 >= X + 0 = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 0 >= 0 = false() a__minus(X1,X2) = X1 + X2 + 0 >= X2 = minus(X1,X2) a__geq(X1,X2) = X1 + X2 >= 4X1 + X2 + 0 = geq(X1,X2) a__div(X1,X2) = X1 + X2 + 0 >= X1 + 4X2 = div(X1,X2) a__if(X1,X2,X3) = X1 + X2 + 0 >= X1 + 4X2 + 2X3 + 2 = if(X1,X2,X3) problem: DPs: 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) 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) Restore Modifier: DPs: 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) 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 usable rules: a__geq(X,0()) -> true() a__geq(0(),s(Y)) -> false() a__geq(s(X),s(Y)) -> a__geq(X,Y) a__geq(X1,X2) -> geq(X1,X2) interpretation: [mark#](x0) = x0, [a__if#](x0, x1, x2) = x0 + x1 + 5x2 + -16, [a__div#](x0, x1) = 3x1, [if](x0, x1, x2) = x2 + 0, [geq](x0, x1) = x1, [mark](x0) = x0 + 0, [a__if](x0, x1, x2) = 0, [div](x0, x1) = 2x0 + 3x1 + 0, [minus](x0, x1) = -8x1 + 2, [a__div](x0, x1) = 2x0 + 2x1 + 0, [false] = 2, [true] = 0, [a__geq](x0, x1) = x1 + 0, [s](x0) = x0 + 2, [a__minus](x0, x1) = -8x0 + x1 + -16, [0] = 0 orientation: mark#(div(X1,X2)) = 2X1 + 3X2 + 0 >= X1 = mark#(X1) mark#(div(X1,X2)) = 2X1 + 3X2 + 0 >= 3X2 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 3Y + 5 >= 3Y + 5 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + 5Y + 0 >= X = mark#(X) a__if#(false(),X,Y) = X + 5Y + 2 >= Y = mark#(Y) mark#(s(X)) = X + 2 >= X = mark#(X) a__minus(0(),Y) = Y + -8 >= 0 = 0() a__minus(s(X),s(Y)) = -8X + Y + 2 >= -8X + Y + -16 = a__minus(X,Y) a__geq(X,0()) = 0 >= 0 = true() a__geq(0(),s(Y)) = Y + 2 >= 2 = false() a__geq(s(X),s(Y)) = Y + 2 >= Y + 0 = a__geq(X,Y) a__div(0(),s(Y)) = 2Y + 4 >= 0 = 0() a__div(s(X),s(Y)) = 2X + 2Y + 4 >= 0 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = 0 >= X + 0 = mark(X) a__if(false(),X,Y) = 0 >= Y + 0 = mark(Y) mark(minus(X1,X2)) = -8X2 + 2 >= -8X1 + X2 + -16 = a__minus(X1,X2) mark(geq(X1,X2)) = X2 + 0 >= X2 + 0 = a__geq(X1,X2) mark(div(X1,X2)) = 2X1 + 3X2 + 0 >= 2X1 + 2X2 + 2 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X3 + 0 >= 0 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 0() mark(s(X)) = X + 2 >= X + 2 = s(mark(X)) mark(true()) = 0 >= 0 = true() mark(false()) = 2 >= 2 = false() a__minus(X1,X2) = -8X1 + X2 + -16 >= -8X2 + 2 = minus(X1,X2) a__geq(X1,X2) = X2 + 0 >= X2 = geq(X1,X2) a__div(X1,X2) = 2X1 + 2X2 + 0 >= 2X1 + 3X2 + 0 = div(X1,X2) a__if(X1,X2,X3) = 0 >= X3 + 0 = 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) Restore Modifier: 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 usable rules: 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) interpretation: [mark#](x0) = x0 + 0, [a__if#](x0, x1, x2) = x1 + 5x2 + 7, [a__div#](x0, x1) = 6x0, [if](x0, x1, x2) = x1 + 7x2, [geq](x0, x1) = x0 + x1, [mark](x0) = x0, [a__if](x0, x1, x2) = x1 + 7x2, [div](x0, x1) = 6x0 + 6, [minus](x0, x1) = x0, [a__div](x0, x1) = 6x0 + 6, [false] = 0, [true] = 0, [a__geq](x0, x1) = x0 + x1, [s](x0) = 1x0 + 1, [a__minus](x0, x1) = x0, [0] = 0 orientation: mark#(div(X1,X2)) = 6X1 + 6 >= 6X1 = a__div#(mark(X1),X2) a__div#(s(X),s(Y)) = 7X + 7 >= 7X + 7 = a__if#(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if#(true(),X,Y) = X + 5Y + 7 >= X + 0 = mark#(X) mark#(s(X)) = 1X + 1 >= X + 0 = mark#(X) a__minus(0(),Y) = 0 >= 0 = 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)) = 1Y + 1 >= 0 = false() a__geq(s(X),s(Y)) = 1X + 1Y + 1 >= X + Y = a__geq(X,Y) a__div(0(),s(Y)) = 6 >= 0 = 0() a__div(s(X),s(Y)) = 7X + 7 >= 7X + 7 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = X + 7Y >= X = mark(X) a__if(false(),X,Y) = X + 7Y >= Y = mark(Y) mark(minus(X1,X2)) = X1 >= X1 = a__minus(X1,X2) mark(geq(X1,X2)) = X1 + X2 >= X1 + X2 = a__geq(X1,X2) mark(div(X1,X2)) = 6X1 + 6 >= 6X1 + 6 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = X2 + 7X3 >= X2 + 7X3 = a__if(mark(X1),X2,X3) mark(0()) = 0 >= 0 = 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 + X2 >= X1 + X2 = geq(X1,X2) a__div(X1,X2) = 6X1 + 6 >= 6X1 + 6 = div(X1,X2) a__if(X1,X2,X3) = X2 + 7X3 >= X2 + 7X3 = 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) Restore Modifier: 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 usable rules: interpretation: [mark#](x0) = -2x0 + 0, [a__if#](x0, x1, x2) = x1 + 4x2 + 1, [a__div#](x0, x1) = -8x1 + 4, [if](x0, x1, x2) = 1x0 + 4x1 + x2 + 0, [geq](x0, x1) = x0 + 5x1, [mark](x0) = 1x0 + 1, [a__if](x0, x1, x2) = 2x1 + 4x2 + 0, [div](x0, x1) = x0 + -6x1 + 6, [minus](x0, x1) = -8x1 + 5, [a__div](x0, x1) = -8x0 + x1 + -16, [false] = 6, [true] = 1, [a__geq](x0, x1) = 4x0 + 4x1 + 2, [s](x0) = 0, [a__minus](x0, x1) = 2x1 + -16, [0] = 0 orientation: mark#(div(X1,X2)) = -2X1 + -8X2 + 4 >= -8X2 + 4 = a__div#(mark(X1),X2) 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) = X + 4Y + 1 >= -2X + 0 = mark#(X) a__minus(0(),Y) = 2Y + -16 >= 0 = 0() a__minus(s(X),s(Y)) = 2 >= 2Y + -16 = a__minus(X,Y) a__geq(X,0()) = 4X + 4 >= 1 = true() a__geq(0(),s(Y)) = 4 >= 6 = false() a__geq(s(X),s(Y)) = 4 >= 4X + 4Y + 2 = a__geq(X,Y) a__div(0(),s(Y)) = 0 >= 0 = 0() a__div(s(X),s(Y)) = 0 >= 4 = a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0()) a__if(true(),X,Y) = 2X + 4Y + 0 >= 1X + 1 = mark(X) a__if(false(),X,Y) = 2X + 4Y + 0 >= 1Y + 1 = mark(Y) mark(minus(X1,X2)) = -7X2 + 6 >= 2X2 + -16 = a__minus(X1,X2) mark(geq(X1,X2)) = 1X1 + 6X2 + 1 >= 4X1 + 4X2 + 2 = a__geq(X1,X2) mark(div(X1,X2)) = 1X1 + -5X2 + 7 >= -7X1 + X2 + -7 = a__div(mark(X1),X2) mark(if(X1,X2,X3)) = 2X1 + 5X2 + 1X3 + 1 >= 2X2 + 4X3 + 0 = a__if(mark(X1),X2,X3) mark(0()) = 1 >= 0 = 0() mark(s(X)) = 1 >= 0 = s(mark(X)) mark(true()) = 2 >= 1 = true() mark(false()) = 7 >= 6 = false() a__minus(X1,X2) = 2X2 + -16 >= -8X2 + 5 = minus(X1,X2) a__geq(X1,X2) = 4X1 + 4X2 + 2 >= X1 + 5X2 = geq(X1,X2) a__div(X1,X2) = -8X1 + X2 + -16 >= X1 + -6X2 + 6 = div(X1,X2) a__if(X1,X2,X3) = 2X2 + 4X3 + 0 >= 1X1 + 4X2 + X3 + 0 = 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()) 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) Restore Modifier: 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()) 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#) = 0 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#) = 0 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