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#() CDG 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__0()) -> 0#() if#(false(),X,Y) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) if#(true(),X,Y) -> activate#(X) -> activate#(n__0()) -> 0#() if#(true(),X,Y) -> activate#(X) -> activate#(n__s(X)) -> s#(X) 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)) -> 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)) -> geq#(X,activate(Y)) -> geq#(n__s(X),n__s(Y)) -> 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)) -> geq#(activate(X),activate(Y)) div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() div#(s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) -> minus#(n__0(),Y) -> 0#() 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__s(X),n__s(Y)) -> activate#(X) div#(s(X),n__s(Y)) -> minus#(X,activate(Y)) -> minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) 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)) -> 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)) -> geq#(activate(X),activate(Y)) geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__0()) -> 0#() geq#(n__s(X),n__s(Y)) -> activate#(Y) -> activate#(n__s(X)) -> s#(X) geq#(n__s(X),n__s(Y)) -> activate#(X) -> activate#(n__0()) -> 0#() geq#(n__s(X),n__s(Y)) -> activate#(X) -> 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#(Y) -> 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)) -> activate#(X) -> activate#(n__s(X)) -> s#(X) minus#(n__s(X),n__s(Y)) -> minus#(activate(X),activate(Y)) -> minus#(n__0(),Y) -> 0#() 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__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)) -> minus#(activate(X),activate(Y)) SCC Processor: #sccs: 2 #rules: 2 #arcs: 30/256 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 Matrix Interpretation Processor: dim=1 interpretation: [minus#](x0, x1) = x0, [if](x0, x1, x2) = x1 + 4x2, [s](x0) = x0 + 2, [div](x0, x1) = x0, [false] = 0, [true] = 0, [geq](x0, x1) = 4x0 + 3, [activate](x0) = x0, [n__s](x0) = x0 + 2, [0] = 0, [minus](x0, x1) = 0, [n__0] = 0 orientation: minus#(n__s(X),n__s(Y)) = X + 2 >= X = minus#(activate(X),activate(Y)) 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()) = 4X + 3 >= 0 = true() geq(n__0(),n__s(Y)) = 3 >= 0 = false() geq(n__s(X),n__s(Y)) = 4X + 11 >= 4X + 3 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 0 >= 0 = 0() div(s(X),n__s(Y)) = X + 2 >= 2 = if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + 4Y >= X = activate(X) if(false(),X,Y) = X + 4Y >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X + 2 >= X + 2 = n__s(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 2 >= X + 2 = 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: 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 Matrix Interpretation Processor: dim=1 interpretation: [geq#](x0, x1) = x0, [if](x0, x1, x2) = x1 + 4x2, [s](x0) = x0 + 2, [div](x0, x1) = x0, [false] = 0, [true] = 0, [geq](x0, x1) = 4x0 + 3, [activate](x0) = x0, [n__s](x0) = x0 + 2, [0] = 0, [minus](x0, x1) = 0, [n__0] = 0 orientation: geq#(n__s(X),n__s(Y)) = X + 2 >= X = geq#(activate(X),activate(Y)) 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()) = 4X + 3 >= 0 = true() geq(n__0(),n__s(Y)) = 3 >= 0 = false() geq(n__s(X),n__s(Y)) = 4X + 11 >= 4X + 3 = geq(activate(X),activate(Y)) div(0(),n__s(Y)) = 0 >= 0 = 0() div(s(X),n__s(Y)) = X + 2 >= 2 = if(geq(X,activate(Y)),n__s(div(minus(X,activate(Y)),n__s(activate(Y)))), n__0()) if(true(),X,Y) = X + 4Y >= X = activate(X) if(false(),X,Y) = X + 4Y >= Y = activate(Y) 0() = 0 >= 0 = n__0() s(X) = X + 2 >= X + 2 = n__s(X) activate(n__0()) = 0 >= 0 = 0() activate(n__s(X)) = X + 2 >= X + 2 = 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