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 Usable Rule Processor: 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: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Arctic Interpretation Processor: dimension: 1 usable rules: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) interpretation: [zWquot#](x0, x1) = x0 + x1 + 0, [activate#](x0) = x0, [n__zWquot](x0, x1) = x0 + x1 + 0, [zWquot](x0, x1) = x0 + x1 + 0, [nil] = 6, [quot](x0, x1) = x0 + x1 + 0, [minus](x0, x1) = x0 + x1 + 0, [activate](x0) = x0, [s](x0) = x0 + 0, [0] = 0, [cons](x0, x1) = x0 + x1 + 0, [n__from](x0) = 1x0 + 1, [n__s](x0) = x0 + 0, [from](x0) = 1x0 + 1 orientation: zWquot#(cons(X,XS),cons(Y,YS)) = X + XS + Y + YS + 0 >= YS = activate#(YS) activate#(n__from(X)) = 1X + 1 >= X = activate#(X) activate#(n__s(X)) = X + 0 >= X = activate#(X) activate#(n__zWquot(X1,X2)) = X1 + X2 + 0 >= X2 = activate#(X2) activate#(n__zWquot(X1,X2)) = X1 + X2 + 0 >= X1 = activate#(X1) activate#(n__zWquot(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) = X + XS + Y + YS + 0 >= XS = activate#(XS) activate(n__from(X)) = 1X + 1 >= 1X + 1 = from(activate(X)) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__zWquot(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = zWquot(activate(X1),activate(X2)) activate(X) = X >= X = X from(X) = 1X + 1 >= 1X + 1 = cons(X,n__from(n__s(X))) from(X) = 1X + 1 >= 1X + 1 = n__from(X) s(X) = X + 0 >= X + 0 = n__s(X) zWquot(XS,nil()) = XS + 6 >= 6 = nil() zWquot(nil(),XS) = XS + 6 >= 6 = nil() zWquot(cons(X,XS),cons(Y,YS)) = X + XS + Y + YS + 0 >= X + XS + Y + YS + 0 = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__zWquot(X1,X2) quot(0(),s(Y)) = Y + 0 >= 0 = 0() quot(s(X),s(Y)) = X + Y + 0 >= X + Y + 0 = s(quot(minus(X,Y),s(Y))) minus(X,0()) = X + 0 >= 0 = 0() minus(s(X),s(Y)) = X + Y + 0 >= X + Y + 0 = minus(X,Y) problem: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Restore Modifier: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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 Usable Rule Processor: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Arctic Interpretation Processor: dimension: 1 usable rules: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) interpretation: [zWquot#](x0, x1) = x0 + x1, [activate#](x0) = x0, [n__zWquot](x0, x1) = x0 + x1, [zWquot](x0, x1) = x0 + x1, [nil] = 2, [quot](x0, x1) = x0 + 0, [minus](x0, x1) = 2x0 + 0, [activate](x0) = x0, [s](x0) = 2x0, [0] = 4, [cons](x0, x1) = x1 + 0, [n__from](x0) = 0, [n__s](x0) = 2x0, [from](x0) = 0 orientation: zWquot#(cons(X,XS),cons(Y,YS)) = XS + YS + 0 >= YS = activate#(YS) activate#(n__s(X)) = 2X >= X = activate#(X) activate#(n__zWquot(X1,X2)) = X1 + X2 >= X2 = activate#(X2) activate#(n__zWquot(X1,X2)) = X1 + X2 >= X1 = activate#(X1) activate#(n__zWquot(X1,X2)) = X1 + X2 >= X1 + X2 = zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) = XS + YS + 0 >= XS = activate#(XS) activate(n__from(X)) = 0 >= 0 = from(activate(X)) activate(n__s(X)) = 2X >= 2X = s(activate(X)) activate(n__zWquot(X1,X2)) = X1 + X2 >= X1 + X2 = zWquot(activate(X1),activate(X2)) activate(X) = X >= X = X from(X) = 0 >= 0 = cons(X,n__from(n__s(X))) from(X) = 0 >= 0 = n__from(X) s(X) = 2X >= 2X = n__s(X) zWquot(XS,nil()) = XS + 2 >= 2 = nil() zWquot(nil(),XS) = XS + 2 >= 2 = nil() zWquot(cons(X,XS),cons(Y,YS)) = XS + YS + 0 >= XS + YS + 0 = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(X1,X2) = X1 + X2 >= X1 + X2 = n__zWquot(X1,X2) quot(0(),s(Y)) = 4 >= 4 = 0() quot(s(X),s(Y)) = 2X + 0 >= 4X + 2 = s(quot(minus(X,Y),s(Y))) minus(X,0()) = 2X + 0 >= 4 = 0() minus(s(X),s(Y)) = 4X + 0 >= 2X + 0 = minus(X,Y) problem: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Restore Modifier: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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 Usable Rule Processor: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Arctic Interpretation Processor: dimension: 1 usable rules: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) interpretation: [zWquot#](x0, x1) = 6x0 + 4x1 + 0, [activate#](x0) = 4x0 + 0, [n__zWquot](x0, x1) = 2x0 + x1 + 2, [zWquot](x0, x1) = 2x0 + x1 + 2, [nil] = 0, [quot](x0, x1) = x0 + 7, [minus](x0, x1) = 7x0 + x1 + 0, [activate](x0) = x0 + 0, [s](x0) = x0 + 0, [0] = 6, [cons](x0, x1) = x1 + 0, [n__from](x0) = 0, [n__s](x0) = x0, [from](x0) = 0 orientation: zWquot#(cons(X,XS),cons(Y,YS)) = 6XS + 4YS + 6 >= 4YS + 0 = activate#(YS) activate#(n__zWquot(X1,X2)) = 6X1 + 4X2 + 6 >= 4X2 + 0 = activate#(X2) activate#(n__zWquot(X1,X2)) = 6X1 + 4X2 + 6 >= 4X1 + 0 = activate#(X1) activate#(n__zWquot(X1,X2)) = 6X1 + 4X2 + 6 >= 6X1 + 4X2 + 6 = zWquot#(activate(X1),activate(X2)) zWquot#(cons(X,XS),cons(Y,YS)) = 6XS + 4YS + 6 >= 4XS + 0 = activate#(XS) activate(n__from(X)) = 0 >= 0 = from(activate(X)) activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X)) activate(n__zWquot(X1,X2)) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = zWquot(activate(X1),activate(X2)) activate(X) = X + 0 >= X = X from(X) = 0 >= 0 = cons(X,n__from(n__s(X))) from(X) = 0 >= 0 = n__from(X) s(X) = X + 0 >= X = n__s(X) zWquot(XS,nil()) = 2XS + 2 >= 0 = nil() zWquot(nil(),XS) = XS + 2 >= 0 = nil() zWquot(cons(X,XS),cons(Y,YS)) = 2XS + YS + 2 >= 2XS + YS + 2 = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(X1,X2) = 2X1 + X2 + 2 >= 2X1 + X2 + 2 = n__zWquot(X1,X2) quot(0(),s(Y)) = 7 >= 6 = 0() quot(s(X),s(Y)) = X + 7 >= 7X + Y + 7 = s(quot(minus(X,Y),s(Y))) minus(X,0()) = 7X + 6 >= 6 = 0() minus(s(X),s(Y)) = 7X + Y + 7 >= 7X + Y + 0 = minus(X,Y) problem: DPs: 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)) TRS: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Restore Modifier: DPs: 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)) 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 Usable Rule Processor: DPs: 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)) TRS: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Arctic Interpretation Processor: dimension: 1 usable rules: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) interpretation: [zWquot#](x0, x1) = 4x0 + 1x1, [activate#](x0) = 1x0, [n__zWquot](x0, x1) = 3x0 + 1x1, [zWquot](x0, x1) = 3x0 + 1x1, [nil] = 0, [quot](x0, x1) = x0 + 1x1 + 4, [minus](x0, x1) = 1x0 + 4x1 + 4, [activate](x0) = x0, [s](x0) = x0, [0] = 0, [cons](x0, x1) = x1, [n__from](x0) = 4x0, [n__s](x0) = x0, [from](x0) = 4x0 orientation: zWquot#(cons(X,XS),cons(Y,YS)) = 4XS + 1YS >= 1YS = activate#(YS) activate#(n__zWquot(X1,X2)) = 4X1 + 2X2 >= 1X2 = activate#(X2) activate#(n__zWquot(X1,X2)) = 4X1 + 2X2 >= 4X1 + 1X2 = zWquot#(activate(X1),activate(X2)) activate(n__from(X)) = 4X >= 4X = from(activate(X)) activate(n__s(X)) = X >= X = s(activate(X)) activate(n__zWquot(X1,X2)) = 3X1 + 1X2 >= 3X1 + 1X2 = zWquot(activate(X1),activate(X2)) activate(X) = X >= X = X from(X) = 4X >= 4X = cons(X,n__from(n__s(X))) from(X) = 4X >= 4X = n__from(X) s(X) = X >= X = n__s(X) zWquot(XS,nil()) = 3XS + 1 >= 0 = nil() zWquot(nil(),XS) = 1XS + 3 >= 0 = nil() zWquot(cons(X,XS),cons(Y,YS)) = 3XS + 1YS >= 3XS + 1YS = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(X1,X2) = 3X1 + 1X2 >= 3X1 + 1X2 = n__zWquot(X1,X2) quot(0(),s(Y)) = 1Y + 4 >= 0 = 0() quot(s(X),s(Y)) = X + 1Y + 4 >= 1X + 4Y + 4 = s(quot(minus(X,Y),s(Y))) minus(X,0()) = 1X + 4 >= 0 = 0() minus(s(X),s(Y)) = 1X + 4Y + 4 >= 1X + 4Y + 4 = minus(X,Y) problem: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) TRS: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Restore Modifier: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) 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 Usable Rule Processor: DPs: zWquot#(cons(X,XS),cons(Y,YS)) -> activate#(YS) activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) TRS: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Arctic Interpretation Processor: dimension: 1 usable rules: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) interpretation: [zWquot#](x0, x1) = x0 + 2x1, [activate#](x0) = x0, [n__zWquot](x0, x1) = 7x0 + 2x1, [zWquot](x0, x1) = 7x0 + 2x1, [nil] = 0, [quot](x0, x1) = 5x1, [minus](x0, x1) = 4x1, [activate](x0) = x0, [s](x0) = 0, [0] = 3, [cons](x0, x1) = x1, [n__from](x0) = 0, [n__s](x0) = 0, [from](x0) = 0 orientation: zWquot#(cons(X,XS),cons(Y,YS)) = XS + 2YS >= YS = activate#(YS) activate#(n__zWquot(X1,X2)) = 7X1 + 2X2 >= X1 + 2X2 = zWquot#(activate(X1),activate(X2)) activate(n__from(X)) = 0 >= 0 = from(activate(X)) activate(n__s(X)) = 0 >= 0 = s(activate(X)) activate(n__zWquot(X1,X2)) = 7X1 + 2X2 >= 7X1 + 2X2 = zWquot(activate(X1),activate(X2)) activate(X) = X >= X = X from(X) = 0 >= 0 = cons(X,n__from(n__s(X))) from(X) = 0 >= 0 = n__from(X) s(X) = 0 >= 0 = n__s(X) zWquot(XS,nil()) = 7XS + 2 >= 0 = nil() zWquot(nil(),XS) = 2XS + 7 >= 0 = nil() zWquot(cons(X,XS),cons(Y,YS)) = 7XS + 2YS >= 7XS + 2YS = cons(quot(X,Y),n__zWquot(activate(XS),activate(YS))) zWquot(X1,X2) = 7X1 + 2X2 >= 7X1 + 2X2 = n__zWquot(X1,X2) quot(0(),s(Y)) = 5 >= 3 = 0() quot(s(X),s(Y)) = 5 >= 0 = s(quot(minus(X,Y),s(Y))) minus(X,0()) = 7 >= 3 = 0() minus(s(X),s(Y)) = 4 >= 4Y = minus(X,Y) problem: DPs: activate#(n__zWquot(X1,X2)) -> zWquot#(activate(X1),activate(X2)) TRS: 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 from(X) -> cons(X,n__from(n__s(X))) from(X) -> n__from(X) s(X) -> n__s(X) 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))) zWquot(X1,X2) -> n__zWquot(X1,X2) quot(0(),s(Y)) -> 0() quot(s(X),s(Y)) -> s(quot(minus(X,Y),s(Y))) minus(X,0()) -> 0() minus(s(X),s(Y)) -> minus(X,Y) Restore Modifier: DPs: 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 SCC Processor: #sccs: 0 #rules: 0 #arcs: 32/1 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