YES Problem: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Proof: DP Processor: DPs: minus#(n__0(),Y) -> 0#() minus#(n__s(X),n__s(Y)) -> activate#(Y) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(Y) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> activate#(Y) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X TDG Processor: DPs: minus#(n__0(),Y) -> 0#() minus#(n__s(X),n__s(Y)) -> activate#(Y) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(Y) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> activate#(Y) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) if#(false(),X,Y) -> activate#(Y) activate#(n__0()) -> 0#() activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X graph: if#(false(),X,Y) -> activate#(Y) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) if#(false(),X,Y) -> activate#(Y) -> activate#(n__div(X1,X2)) -> activate#(X1) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__0()) -> 0#() if#(true(),X,Y) -> activate#(X) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) if#(true(),X,Y) -> activate#(X) -> activate#(n__div(X1,X2)) -> activate#(X1) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__0()) -> 0#() div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) -> if#(false(),X,Y) -> activate#(Y) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) -> if#(true(),X,Y) -> activate#(X) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) -> geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) -> geq#(n__s(X),n__s(Y)) -> activate#(X) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) -> geq#(n__s(X),n__s(Y)) -> activate#(Y) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__div(X1,X2)) -> activate#(X1) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) -> geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) -> geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) -> geq#(n__s(X),n__s(Y)) -> activate#(Y) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__div(X1,X2)) -> activate#(X1) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__div(X1,X2)) -> activate#(X1) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__0()) -> 0#() activate#(n__div(X1,X2)) -> div#(activate(X1),X2) -> div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) -> div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) -> div#(s(X),n__s(Y)) -> activate#(Y) activate#(n__div(X1,X2)) -> activate#(X1) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) activate#(n__div(X1,X2)) -> activate#(X1) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__div(X1,X2)) -> activate#(X1) -> activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__div(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> activate#(X1) -> activate#(n__0()) -> 0#() activate#(n__minus(X1,X2)) -> minus#(X1,X2) -> minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) activate#(n__minus(X1,X2)) -> minus#(X1,X2) -> minus#(n__s(X),n__s(Y)) -> activate#(X) activate#(n__minus(X1,X2)) -> minus#(X1,X2) -> minus#(n__s(X),n__s(Y)) -> activate#(Y) activate#(n__minus(X1,X2)) -> minus#(X1,X2) -> minus#(n__0(),Y) -> 0#() activate#(n__s(X)) -> activate#(X) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__s(X)) -> activate#(X) -> activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__0()) -> 0#() minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__div(X1,X2)) -> activate#(X1) minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(activate(X)) minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() minus#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__div(X1,X2)) -> div#(activate(X1),X2) minus#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__div(X1,X2)) -> activate#(X1) minus#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) minus#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__0()) -> 0#() minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) -> minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) -> minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) -> minus#(n__s(X),n__s(Y)) -> activate#(Y) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) -> minus#(n__0(),Y) -> 0#() SCC Processor: #sccs: 1 #rules: 15 #arcs: 73/324 DPs: if#(false(),X,Y) -> activate#(Y) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) div#(s(X),n__s(Y)) -> activate#(Y) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(Y) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(Y) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [if#](x0, x1, x2) = x1 + x2 + 0, [div#](x0, x1) = x0 + 3x1 + 0, [geq#](x0, x1) = x0 + 3x1 + 0, [activate#](x0) = x0, [minus#](x0, x1) = x0 + 2x1, [if](x0, x1, x2) = x1 + x2 + 0, [n__div](x0, x1) = x0 + 3x1 + 0, [n__minus](x0, x1) = x0 + 2x1 + 0, [s](x0) = x0, [div](x0, x1) = x0 + 3x1 + 0, [false] = 2, [true] = 0, [geq](x0, x1) = x0 + x1 + 0, [activate](x0) = x0, [n__s](x0) = x0, [0] = 0, [minus](x0, x1) = x0 + 2x1 + 0, [n__0] = 0 orientation: if#(false(),X,Y) = X + Y + 0 >= Y = activate#(Y) activate#(n__s(X)) = X >= X = activate#(X) activate#(n__div(X1,X2)) = X1 + 3X2 + 0 >= X1 = activate#(X1) activate#(n__div(X1,X2)) = X1 + 3X2 + 0 >= X1 + 3X2 + 0 = div#(activate(X1),X2) div#(s(X),n__s(Y)) = X + 3Y + 0 >= Y = activate#(Y) activate#(n__minus(X1,X2)) = X1 + 2X2 + 0 >= X1 + 2X2 = minus#(X1,X2) minus#(n__s(X),n__s(Y)) = X + 2Y >= Y = activate#(Y) minus#(n__s(X),n__s(Y)) = X + 2Y >= X = activate#(X) minus#(n__s(X),n__s(Y)) = X + 2Y >= X + 2Y = minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) = X + 3Y + 0 >= Y = activate#(Y) geq#(n__s(X),n__s(Y)) = X + 3Y + 0 >= X = activate#(X) geq#(n__s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if#(true(),X,Y) = X + Y + 0 >= X = activate#(X) minus(n__0(),Y) = 2Y + 0 >= 0 = 0() minus(n__s(X),n__s(Y)) = X + 2Y + 0 >= X + 2Y + 0 = minus(activate(X),activate(Y)) geq(X,n__0()) = X + 0 >= 0 = true() geq(n__0(),n__s(Y)) = Y + 0 >= 2 = false() geq(n__s(X),n__s(Y)) = X + Y + 0 >= X + Y + 0 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 3Y + 0 >= 0 = 0() div(s(X),n__s(Y)) = X + 3Y + 0 >= X + 3Y + 0 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X >= X = n__s(X) div(X1,X2) = X1 + 3X2 + 0 >= X1 + 3X2 + 0 = n__div(X1,X2) minus(X1,X2) = X1 + 2X2 + 0 >= X1 + 2X2 + 0 = n__minus(X1,X2) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X >= X = s(activate(X)) activate(n__div(X1,X2)) = X1 + 3X2 + 0 >= X1 + 3X2 + 0 = div(activate(X1),X2) activate(n__minus(X1,X2)) = X1 + 2X2 + 0 >= X1 + 2X2 + 0 = minus(X1,X2) activate(X) = X >= X = X problem: DPs: if#(false(),X,Y) -> activate#(Y) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Restore Modifier: DPs: if#(false(),X,Y) -> activate#(Y) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [if#](x0, x1, x2) = x1 + 7x2 + 6, [div#](x0, x1) = x0 + 7x1 + 7, [geq#](x0, x1) = x0 + 7, [activate#](x0) = x0 + 0, [minus#](x0, x1) = x0 + 0, [if](x0, x1, x2) = x1 + 7x2, [n__div](x0, x1) = x0 + 7x1 + 7, [n__minus](x0, x1) = x0 + x1 + 0, [s](x0) = x0 + 0, [div](x0, x1) = x0 + 7x1 + 7, [false] = 4, [true] = 4, [geq](x0, x1) = x1, [activate](x0) = x0, [n__s](x0) = x0 + 0, [0] = 0, [minus](x0, x1) = x0 + x1 + 0, [n__0] = 0 orientation: if#(false(),X,Y) = X + 7Y + 6 >= Y + 0 = activate#(Y) activate#(n__s(X)) = X + 0 >= X + 0 = activate#(X) activate#(n__div(X1,X2)) = X1 + 7X2 + 7 >= X1 + 0 = activate#(X1) activate#(n__div(X1,X2)) = X1 + 7X2 + 7 >= X1 + 7X2 + 7 = div#(activate(X1),X2) activate#(n__minus(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = minus#(X1,X2) minus#(n__s(X),n__s(Y)) = X + 0 >= X + 0 = activate#(X) minus#(n__s(X),n__s(Y)) = X + 0 >= X + 0 = minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) = X + 7Y + 7 >= X + 7 = geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) = X + 7 >= X + 0 = activate#(X) geq#(n__s(X),n__s(Y)) = X + 7 >= X + 7 = geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) = X + 7Y + 7 >= X + 7Y + 7 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if#(true(),X,Y) = X + 7Y + 6 >= X + 0 = activate#(X) minus(n__0(),Y) = Y + 0 >= 0 = 0() minus(n__s(X),n__s(Y)) = X + Y + 0 >= X + Y + 0 = minus(activate(X),activate(Y)) geq(X,n__0()) = 0 >= 4 = true() geq(n__0(),n__s(Y)) = Y + 0 >= 4 = false() geq(n__s(X),n__s(Y)) = Y + 0 >= Y = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 7Y + 7 >= 0 = 0() div(s(X),n__s(Y)) = X + 7Y + 7 >= X + 7Y + 7 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + 7Y >= X = activate(X) if(false(),X,Y) = X + 7Y >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X + 0 = n__s(X) div(X1,X2) = X1 + 7X2 + 7 >= X1 + 7X2 + 7 = n__div(X1,X2) minus(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__minus(X1,X2) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__div(X1,X2)) = X1 + 7X2 + 7 >= X1 + 7X2 + 7 = div(activate(X1),X2) activate(n__minus(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = minus(X1,X2) activate(X) = X >= X = X problem: DPs: activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Restore Modifier: DPs: activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> activate#(X1) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [if#](x0, x1, x2) = x1 + 4x2 + 0, [div#](x0, x1) = 4x0 + 6x1, [geq#](x0, x1) = x0, [activate#](x0) = x0, [minus#](x0, x1) = x0, [if](x0, x1, x2) = x1 + 2x2 + 0, [n__div](x0, x1) = 4x0 + 6x1 + 0, [n__minus](x0, x1) = x0, [s](x0) = x0 + 0, [div](x0, x1) = 4x0 + 6x1 + 0, [false] = 2, [true] = 2, [geq](x0, x1) = 4x1 + 0, [activate](x0) = x0, [n__s](x0) = x0 + 0, [0] = 0, [minus](x0, x1) = x0, [n__0] = 0 orientation: activate#(n__s(X)) = X + 0 >= X = activate#(X) activate#(n__div(X1,X2)) = 4X1 + 6X2 + 0 >= X1 = activate#(X1) activate#(n__div(X1,X2)) = 4X1 + 6X2 + 0 >= 4X1 + 6X2 = div#(activate(X1),X2) activate#(n__minus(X1,X2)) = X1 >= X1 = minus#(X1,X2) minus#(n__s(X),n__s(Y)) = X + 0 >= X = activate#(X) minus#(n__s(X),n__s(Y)) = X + 0 >= X = minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) = 4X + 6Y + 6 >= X = geq#(X,activate(Y)) geq#(n__s(X),n__s(Y)) = X + 0 >= X = activate#(X) geq#(n__s(X),n__s(Y)) = X + 0 >= X = geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) = 4X + 6Y + 6 >= 4X + 6Y + 6 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if#(true(),X,Y) = X + 4Y + 0 >= X = activate#(X) minus(n__0(),Y) = 0 >= 0 = 0() minus(n__s(X),n__s(Y)) = X + 0 >= X = minus(activate(X),activate(Y)) geq(X,n__0()) = 4 >= 2 = true() geq(n__0(),n__s(Y)) = 4Y + 4 >= 2 = false() geq(n__s(X),n__s(Y)) = 4Y + 4 >= 4Y + 0 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 6Y + 6 >= 0 = 0() div(s(X),n__s(Y)) = 4X + 6Y + 6 >= 4X + 6Y + 6 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + 2Y + 0 >= X = activate(X) if(false(),X,Y) = X + 2Y + 0 >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X + 0 = n__s(X) div(X1,X2) = 4X1 + 6X2 + 0 >= 4X1 + 6X2 + 0 = n__div(X1,X2) minus(X1,X2) = X1 >= X1 = n__minus(X1,X2) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__div(X1,X2)) = 4X1 + 6X2 + 0 >= 4X1 + 6X2 + 0 = div(activate(X1),X2) activate(n__minus(X1,X2)) = X1 >= X1 = minus(X1,X2) activate(X) = X >= X = X problem: DPs: activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Restore Modifier: DPs: activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(X) geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if#(true(),X,Y) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X SCC Processor: #sccs: 2 #rules: 8 #arcs: 53/81 DPs: geq#(n__s(X),n__s(Y)) -> geq#(activate(X),activate(Y)) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [geq#](x0, x1) = x0 + x1 + 0, [if](x0, x1, x2) = x1 + x2 + 0, [n__div](x0, x1) = x0 + 0, [n__minus](x0, x1) = x0 + 3, [s](x0) = 1x0 + 4, [div](x0, x1) = x0 + 0, [false] = 2, [true] = 1, [geq](x0, x1) = 0, [activate](x0) = x0, [n__s](x0) = 1x0 + 4, [0] = 4, [minus](x0, x1) = x0 + 3, [n__0] = 4 orientation: geq#(n__s(X),n__s(Y)) = 1X + 1Y + 4 >= X + Y + 0 = geq#(activate(X),activate(Y)) minus(n__0(),Y) = 4 >= 4 = 0() minus(n__s(X),n__s(Y)) = 1X + 4 >= X + 3 = minus(activate(X),activate(Y)) geq(X,n__0()) = 0 >= 1 = true() geq(n__0(),n__s(Y)) = 0 >= 2 = false() geq(n__s(X),n__s(Y)) = 0 >= 0 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 4 >= 4 = 0() div(s(X),n__s(Y)) = 1X + 4 >= 1X + 4 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) 0() = 4 >= 4 = n__0() s(X) = 1X + 4 >= 1X + 4 = n__s(X) div(X1,X2) = X1 + 0 >= X1 + 0 = n__div(X1,X2) minus(X1,X2) = X1 + 3 >= X1 + 3 = n__minus(X1,X2) activate(n__0()) = 4 >= 4 = 0() activate(n__s(X)) = 1X + 4 >= 1X + 4 = s(activate(X)) activate(n__div(X1,X2)) = X1 + 0 >= X1 + 0 = div(activate(X1),X2) activate(n__minus(X1,X2)) = X1 + 3 >= X1 + 3 = minus(X1,X2) activate(X) = X >= X = X problem: DPs: TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Qed DPs: if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) activate#(n__minus(X1,X2)) -> minus#(X1,X2) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [if#](x0, x1, x2) = x1 + x2, [div#](x0, x1) = x1, [activate#](x0) = x0, [minus#](x0, x1) = x0 + x1 + 0, [if](x0, x1, x2) = x1 + x2 + 0, [n__div](x0, x1) = x1, [n__minus](x0, x1) = 4x0 + 1x1 + 4, [s](x0) = x0 + 0, [div](x0, x1) = x1, [false] = 2, [true] = 4, [geq](x0, x1) = 5x0 + 7x1 + 0, [activate](x0) = x0 + 0, [n__s](x0) = x0 + 0, [0] = 0, [minus](x0, x1) = 4x0 + 1x1 + 4, [n__0] = 0 orientation: if#(true(),X,Y) = X + Y >= X = activate#(X) activate#(n__s(X)) = X + 0 >= X = activate#(X) activate#(n__div(X1,X2)) = X2 >= X2 = div#(activate(X1),X2) div#(s(X),n__s(Y)) = Y + 0 >= Y + 0 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) activate#(n__minus(X1,X2)) = 4X1 + 1X2 + 4 >= X1 + X2 + 0 = minus#(X1,X2) minus#(n__s(X),n__s(Y)) = X + Y + 0 >= X = activate#(X) minus#(n__s(X),n__s(Y)) = X + Y + 0 >= X + Y + 0 = minus#(activate(X),activate(Y)) minus(n__0(),Y) = 1Y + 4 >= 0 = 0() minus(n__s(X),n__s(Y)) = 4X + 1Y + 4 >= 4X + 1Y + 4 = minus(activate(X),activate(Y)) geq(X,n__0()) = 5X + 7 >= 4 = true() geq(n__0(),n__s(Y)) = 7Y + 7 >= 2 = false() geq(n__s(X),n__s(Y)) = 5X + 7Y + 7 >= 5X + 7Y + 7 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = Y + 0 >= 0 = 0() div(s(X),n__s(Y)) = Y + 0 >= Y + 0 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + Y + 0 >= X + 0 = activate(X) if(false(),X,Y) = X + Y + 0 >= Y + 0 = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X + 0 >= X + 0 = n__s(X) div(X1,X2) = X2 >= X2 = n__div(X1,X2) minus(X1,X2) = 4X1 + 1X2 + 4 >= 4X1 + 1X2 + 4 = n__minus(X1,X2) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__div(X1,X2)) = X2 + 0 >= X2 = div(activate(X1),X2) activate(n__minus(X1,X2)) = 4X1 + 1X2 + 4 >= 4X1 + 1X2 + 4 = minus(X1,X2) activate(X) = X + 0 >= X = X problem: DPs: if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Restore Modifier: DPs: if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) minus#(n__s(X),n__s(Y)) -> activate#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X SCC Processor: #sccs: 2 #rules: 5 #arcs: 15/36 DPs: minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [minus#](x0, x1) = x0 + x1 + 0, [if](x0, x1, x2) = x1 + x2 + 0, [n__div](x0, x1) = x0 + 0, [n__minus](x0, x1) = x0 + 3, [s](x0) = 1x0 + 4, [div](x0, x1) = x0 + 0, [false] = 2, [true] = 1, [geq](x0, x1) = 0, [activate](x0) = x0, [n__s](x0) = 1x0 + 4, [0] = 4, [minus](x0, x1) = x0 + 3, [n__0] = 4 orientation: minus#(n__s(X),n__s(Y)) = 1X + 1Y + 4 >= X + Y + 0 = minus#(activate(X),activate(Y)) minus(n__0(),Y) = 4 >= 4 = 0() minus(n__s(X),n__s(Y)) = 1X + 4 >= X + 3 = minus(activate(X),activate(Y)) geq(X,n__0()) = 0 >= 1 = true() geq(n__0(),n__s(Y)) = 0 >= 2 = false() geq(n__s(X),n__s(Y)) = 0 >= 0 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 4 >= 4 = 0() div(s(X),n__s(Y)) = 1X + 4 >= 1X + 4 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + Y + 0 >= X = activate(X) if(false(),X,Y) = X + Y + 0 >= Y = activate(Y) 0() = 4 >= 4 = n__0() s(X) = 1X + 4 >= 1X + 4 = n__s(X) div(X1,X2) = X1 + 0 >= X1 + 0 = n__div(X1,X2) minus(X1,X2) = X1 + 3 >= X1 + 3 = n__minus(X1,X2) activate(n__0()) = 4 >= 4 = 0() activate(n__s(X)) = 1X + 4 >= 1X + 4 = s(activate(X)) activate(n__div(X1,X2)) = X1 + 0 >= X1 + 0 = div(activate(X1),X2) activate(n__minus(X1,X2)) = X1 + 3 >= X1 + 3 = minus(X1,X2) activate(X) = X >= X = X problem: DPs: TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Qed DPs: if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__div(X1,X2)) -> div#(activate(X1),X2) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Arctic Interpretation Processor: dimension: 1 usable rules: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X interpretation: [if#](x0, x1, x2) = 1x0 + x1 + 6x2 + 0, [div#](x0, x1) = x0, [activate#](x0) = x0 + 4, [if](x0, x1, x2) = x1 + 7x2 + 0, [n__div](x0, x1) = 1x0 + 0, [n__minus](x0, x1) = 0, [s](x0) = x0 + 6, [div](x0, x1) = 1x0 + 0, [false] = 0, [true] = 3, [geq](x0, x1) = 3, [activate](x0) = x0, [n__s](x0) = x0 + 6, [0] = 0, [minus](x0, x1) = 0, [n__0] = 0 orientation: if#(true(),X,Y) = X + 6Y + 4 >= X + 4 = activate#(X) activate#(n__s(X)) = X + 6 >= X + 4 = activate#(X) activate#(n__div(X1,X2)) = 1X1 + 4 >= X1 = div#(activate(X1),X2) div#(s(X),n__s(Y)) = X + 6 >= 6 = if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) minus(n__0(),Y) = 0 >= 0 = 0() minus(n__s(X),n__s(Y)) = 0 >= 0 = minus(activate(X),activate(Y)) geq(X,n__0()) = 3 >= 3 = true() geq(n__0(),n__s(Y)) = 3 >= 0 = false() geq(n__s(X),n__s(Y)) = 3 >= 3 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 1 >= 0 = 0() div(s(X),n__s(Y)) = 1X + 7 >= 7 = if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + 7Y + 0 >= X = activate(X) if(false(),X,Y) = X + 7Y + 0 >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X + 6 >= X + 6 = n__s(X) div(X1,X2) = 1X1 + 0 >= 1X1 + 0 = n__div(X1,X2) minus(X1,X2) = 0 >= 0 = n__minus(X1,X2) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 6 >= X + 6 = s(activate(X)) activate(n__div(X1,X2)) = 1X1 + 0 >= 1X1 + 0 = div(activate(X1),X2) activate(n__minus(X1,X2)) = 0 >= 0 = minus(X1,X2) activate(X) = X >= X = X problem: DPs: if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Restore Modifier: DPs: if#(true(),X,Y) -> activate#(X) activate#(n__s(X)) -> activate#(X) div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X SCC Processor: #sccs: 1 #rules: 1 #arcs: 6/9 DPs: activate#(n__s(X)) -> activate#(X) TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Subterm Criterion Processor: simple projection: pi(activate#) = 0 problem: DPs: TRS: minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) -> activate(X) if(false(),X,Y) -> activate(Y) 0() -> n__0() s(X) -> n__s(X) div(X1,X2) -> n__div(X1,X2) minus(X1,X2) -> n__minus(X1,X2) activate(n__0()) -> 0() activate(n__s(X)) -> s(activate(X)) activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(X) -> X Qed