YES Problem: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Proof: DP Processor: DPs: sel#(s(N),cons(X,XS)) -> activate#(XS) sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) minus#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) quot#(s(X),s(Y)) -> s#(quot(minus(X,Y),s(Y))) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) zWquot#(cons(X,XS),cons(Y,YS)) -> quot#(X,Y) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__zWquot(X1,X2)) -> activate#(X2) activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X TDG Processor: DPs: sel#(s(N),cons(X,XS)) -> activate#(XS) sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) minus#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) quot#(s(X),s(Y)) -> s#(quot(minus(X,Y),s(Y))) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) zWquot#(cons(X,XS),cons(Y,YS)) -> quot#(X,Y) activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) activate#(n__s(X)) -> s#(activate(X)) activate#(n__zWquot(X1,X2)) -> activate#(X2) activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X graph: zWquot#(cons(X,XS),cons(Y,YS)) -> quot#(X,Y) -> quot#(s(X),s(Y)) -> s#(quot(minus(X,Y),s(Y))) zWquot#(cons(X,XS),cons(Y,YS)) -> quot#(X,Y) -> quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) zWquot#(cons(X,XS),cons(Y,YS)) -> quot#(X,Y) -> quot#(s(X),s(Y)) -> minus#(X,Y) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__s(X)) -> s#(activate(X)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__s(X)) -> activate#(X) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__from(X)) -> from#(activate(X)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) -> activate#(n__from(X)) -> activate#(X) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__s(X)) -> s#(activate(X)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__s(X)) -> activate#(X) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__from(X)) -> from#(activate(X)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) -> activate#(n__from(X)) -> activate#(X) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) -> quot#(s(X),s(Y)) -> s#(quot(minus(X,Y),s(Y))) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) -> quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) -> quot#(s(X),s(Y)) -> minus#(X,Y) quot#(s(X),s(Y)) -> minus#(X,Y) -> minus#(s(X),s(Y)) -> minus#(X,Y) minus#(s(X),s(Y)) -> minus#(X,Y) -> minus#(s(X),s(Y)) -> minus#(X,Y) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) -> zWquot#(cons(X,XS),cons(Y,YS)) -> quot#(X,Y) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) -> zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) -> zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__s(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__zWquot(X1,X2)) -> activate#(X2) -> activate#(n__from(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__s(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__zWquot(X1,X2)) -> activate#(X1) -> activate#(n__from(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) activate#(n__from(X)) -> activate#(X) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__from(X)) -> activate#(X) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> s#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__s(X)) -> activate#(X) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> from#(activate(X)) activate#(n__from(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) activate#(n__s(X)) -> activate#(X) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__s(X)) -> activate#(X) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) 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__from(X)) -> from#(activate(X)) activate#(n__s(X)) -> activate#(X) -> activate#(n__from(X)) -> activate#(X) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__zWquot(X1,X2)) -> activate#(X1) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__zWquot(X1,X2)) -> activate#(X2) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__s(X)) -> s#(activate(X)) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__s(X)) -> activate#(X) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__from(X)) -> from#(activate(X)) sel#(s(N),cons(X,XS)) -> activate#(XS) -> activate#(n__from(X)) -> activate#(X) sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) -> sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) -> sel#(s(N),cons(X,XS)) -> activate#(XS) SCC Processor: #sccs: 4 #rules: 10 #arcs: 62/256 DPs: sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(sel#) = 0 problem: DPs: TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Qed DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) activate#(n__from(X)) -> activate#(X) activate#(n__s(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X2) activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [zWquot#](x0, x1) = x0 + 4x1, [activate#](x0) = x0, [n__zWquot](x0, x1) = x0 + 4x1, [zWquot](x0, x1) = x0 + 4x1, [nil] = 2, [quot](x0, x1) = x0 + x1, [minus](x0, x1) = x0 + x1, [activate](x0) = x0, [s](x0) = x0, [sel](x0, x1) = x0 + x1 + 0, [0] = 1, [cons](x0, x1) = x0 + x1, [n__from](x0) = 6x0, [n__s](x0) = x0, [from](x0) = 6x0 orientation: zWquot#(cons(X,XS),cons(Y,YS)) = X + XS + 4Y + 4YS >= YS = activate#(YS) activate#(n__from(X)) = 6X >= X = activate#(X) activate#(n__s(X)) = X >= X = activate#(X) activate#(n__zWquot(X1,X2)) = X1 + 4X2 >= X2 = activate#(X2) activate#(n__zWquot(X1,X2)) = X1 + 4X2 >= X1 = activate#(X1) activate#(n__zWquot(X1,X2)) = X1 + 4X2 >= X1 + 4X2 = zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) = X + XS + 4Y + 4YS >= XS = activate#(XS) from(X) = 6X >= 6X = cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) = X + XS + 1 >= X = X sel(s(N),cons(X,XS)) = N + X + XS + 0 >= N + XS + 0 = sel(N,activate(XS)) minus(X,0()) = X + 1 >= 1 = 0() minus(s(X),s(Y)) = X + Y >= X + Y = minus(X,Y) quot(0(),s(Y)) = Y + 1 >= 1 = 0() quot(s(X),s(Y)) = X + Y >= X + Y = s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) = XS + 6 >= 2 = nil() zWquot(nil(),XS) = 4XS + 2 >= 2 = nil() zWquot(cons(X,XS),cons(Y,YS)) = X + XS + 4Y + 4YS >= X + XS + Y + 4YS = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) = 6X >= 6X = n__from(X) s(X) = X >= X = n__s(X) zWquot(X1,X2) = X1 + 4X2 >= X1 + 4X2 = n__zWquot(X1,X2) activate(n__from(X)) = 6X >= 6X = from(activate(X)) activate(n__s(X)) = X >= X = s(activate(X)) activate(n__zWquot(X1,X2)) = X1 + 4X2 >= X1 + 4X2 = zWquot(activate(X1),activate(X2)) activate(X) = X >= X = X problem: DPs: activate#(n__s(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X1) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [zWquot#](x0, x1) = x0 + 2x1 + 0, [activate#](x0) = x0 + 6, [n__zWquot](x0, x1) = 1x0 + 3x1 + 3, [zWquot](x0, x1) = 1x0 + 3x1 + 3, [nil] = 4, [quot](x0, x1) = 1x1 + 0, [minus](x0, x1) = x0 + x1 + 0, [activate](x0) = x0 + 0, [s](x0) = x0 + 0, [sel](x0, x1) = 1x1 + 0, [0] = 1, [cons](x0, x1) = x0 + x1 + 4, [n__from](x0) = 6x0 + 6, [n__s](x0) = x0 + 0, [from](x0) = 6x0 + 6 orientation: activate#(n__s(X)) = X + 6 >= X + 6 = activate#(X) activate#(n__zWquot(X1,X2)) = 1X1 + 3X2 + 6 >= X1 + 6 = activate#(X1) activate#(n__zWquot(X1,X2)) = 1X1 + 3X2 + 6 >= X1 + 2X2 + 2 = zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) = X + XS + 2Y + 2YS + 6 >= XS + 6 = activate#(XS) from(X) = 6X + 6 >= 6X + 6 = cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) = 1X + 1XS + 5 >= X = X sel(s(N),cons(X,XS)) = 1X + 1XS + 5 >= 1XS + 1 = sel(N,activate(XS)) minus(X,0()) = X + 1 >= 1 = 0() minus(s(X),s(Y)) = X + Y + 0 >= X + Y + 0 = minus(X,Y) quot(0(),s(Y)) = 1Y + 1 >= 1 = 0() quot(s(X),s(Y)) = 1Y + 1 >= 1Y + 1 = s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) = 1XS + 7 >= 4 = nil() zWquot(nil(),XS) = 3XS + 5 >= 4 = nil() zWquot(cons(X,XS),cons(Y,YS)) = 1X + 1XS + 3Y + 3YS + 7 >= 1XS + 1Y + 3YS + 4 = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) = 6X + 6 >= 6X + 6 = n__from(X) s(X) = X + 0 >= X + 0 = n__s(X) zWquot(X1,X2) = 1X1 + 3X2 + 3 >= 1X1 + 3X2 + 3 = n__zWquot(X1,X2) activate(n__from(X)) = 6X + 6 >= 6X + 6 = from(activate(X)) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__zWquot(X1,X2)) = 1X1 + 3X2 + 3 >= 1X1 + 3X2 + 3 = zWquot(activate(X1),activate(X2)) activate(X) = X + 0 >= X = X problem: DPs: activate#(n__s(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X1) zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(XS) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X SCC Processor: #sccs: 1 #rules: 2 #arcs: 32/9 DPs: activate#(n__s(X)) -> activate#(X) activate#(n__zWquot(X1,X2)) -> activate#(X1) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(activate#) = 0 problem: DPs: TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Qed DPs: quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X CDG Processor: DPs: quot#(s(X),s(Y)) -> quot#(minus(X,Y),s(Y)) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X graph: Qed DPs: minus#(s(X),s(Y)) -> minus#(X,Y) TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Subterm Criterion Processor: simple projection: pi(minus#) = 1 problem: DPs: TRS: from(X) -> cons(X,n__from(n__s(X))) sel(0(),cons(X,XS)) -> X sel(s(N),cons(X,XS)) -> sel(N,activate(XS)) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) zWquot(XS,nil()) -> nil() zWquot(nil(),XS) -> nil() zWquot(cons(X,XS),cons(Y,YS)) -> cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) from(X) -> n__from(X) s(X) -> n__s(X) zWquot(X1,X2) -> n__zWquot(X1,X2) activate(n__from(X)) -> from(activate(X)) activate(n__s(X)) -> s(activate(X)) activate(n__zWquot(X1,X2)) -> zWquot(activate(X1),activate(X2)) activate(X) -> X Qed