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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) 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)) -> minus#(X,activate(Y)) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(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(div(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)) -> s#(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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) 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)) -> minus#(X,activate(Y)) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(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(div(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)) -> s#(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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X graph: if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) if#(false(),X,Y) -> activate#(Y) -> activate#(n__0()) -> 0#() if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> s#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__0()) -> 0#() div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(div(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(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0()) -> if#(true(),X,Y) -> activate#(X) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(activate(Y))) -> div#(s(X),n__s(Y)) -> if#(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0()) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(activate(Y))) -> div#(s(X),n__s(Y)) -> geq#(X,activate(Y)) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(activate(Y))) -> div#(s(X),n__s(Y)) -> activate#(Y) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(activate(Y))) -> div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(activate(Y))) div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(activate(Y))) -> div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) 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__s(X)) -> s#(X) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) -> minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) -> minus#(n__s(X),n__s(Y)) -> activate#(X) div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) -> minus#(n__s(X),n__s(Y)) -> activate#(Y) div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) -> minus#(n__0(),Y) -> 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__s(X)) -> s#(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__s(X)) -> s#(X) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__0()) -> 0#() minus#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(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__s(X)) -> s#(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: 3 #rules: 3 #arcs: 35/256 DPs: div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X CDG Processor: DPs: div#(s(X),n__s(Y)) -> div#(minus(X,activate(Y)),n__s(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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X graph: Qed 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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [geq#](x0, x1) = x0 + x1, [if](x0, x1, x2) = x1 + x2, [s](x0) = 2x0 + 0, [div](x0, x1) = x0, [false] = 2, [true] = 1, [geq](x0, x1) = 2x1, [activate](x0) = x0, [n__s](x0) = 2x0 + 0, [0] = 0, [minus](x0, x1) = x0, [n__0] = 0 orientation: geq#(n__s(X),n__s(Y)) = 2X + 2Y + 0 >= X + Y = geq#(activate(X),activate(Y)) minus(n__0(),Y) = 0 >= 0 = 0() minus(n__s(X),n__s(Y)) = 2X + 0 >= X = minus(activate(X),activate(Y)) geq(X,n__0()) = 2 >= 1 = true() geq(n__0(),n__s(Y)) = 4Y + 2 >= 2 = false() geq(n__s(X),n__s(Y)) = 4Y + 2 >= 2Y = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 0 >= 0 = 0() div(s(X),n__s(Y)) = 2X + 0 >= 2X + 0 = if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + Y >= X = activate(X) if(false(),X,Y) = X + Y >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = 2X + 0 >= 2X + 0 = n__s(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = 2X + 0 >= 2X + 0 = s(X) 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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X Qed 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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [minus#](x0, x1) = x0 + x1, [if](x0, x1, x2) = x1 + x2, [s](x0) = 2x0 + 0, [div](x0, x1) = x0, [false] = 2, [true] = 1, [geq](x0, x1) = 2x1, [activate](x0) = x0, [n__s](x0) = 2x0 + 0, [0] = 0, [minus](x0, x1) = x0, [n__0] = 0 orientation: minus#(n__s(X),n__s(Y)) = 2X + 2Y + 0 >= X + Y = minus#(activate(X),activate(Y)) minus(n__0(),Y) = 0 >= 0 = 0() minus(n__s(X),n__s(Y)) = 2X + 0 >= X = minus(activate(X),activate(Y)) geq(X,n__0()) = 2 >= 1 = true() geq(n__0(),n__s(Y)) = 4Y + 2 >= 2 = false() geq(n__s(X),n__s(Y)) = 4Y + 2 >= 2Y = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 0 >= 0 = 0() div(s(X),n__s(Y)) = 2X + 0 >= 2X + 0 = if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + Y >= X = activate(X) if(false(),X,Y) = X + Y >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = 2X + 0 >= 2X + 0 = n__s(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = 2X + 0 >= 2X + 0 = s(X) 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(div(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) activate(n__0()) -> 0() activate(n__s(X)) -> s(X) activate(X) -> X Qed