YES Problem: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Proof: DP Processor: DPs: t#(N) -> q#(N) q#(s(X)) -> d#(X) q#(s(X)) -> q#(X) q#(s(X)) -> p#(q(X),d(X)) q#(s(X)) -> s#(p(q(X),d(X))) d#(s(X)) -> d#(X) d#(s(X)) -> s#(d(X)) d#(s(X)) -> s#(s(d(X))) p#(s(X),s(Y)) -> p#(X,Y) p#(s(X),s(Y)) -> s#(p(X,Y)) p#(s(X),s(Y)) -> s#(s(p(X,Y))) f#(s(X),cs(Y,Z)) -> a#(Z) a#(nt(X)) -> a#(X) a#(nt(X)) -> t#(a(X)) a#(ns(X)) -> a#(X) a#(ns(X)) -> s#(a(X)) a#(nf(X1,X2)) -> a#(X2) a#(nf(X1,X2)) -> a#(X1) a#(nf(X1,X2)) -> f#(a(X1),a(X2)) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X TDG Processor: DPs: t#(N) -> q#(N) q#(s(X)) -> d#(X) q#(s(X)) -> q#(X) q#(s(X)) -> p#(q(X),d(X)) q#(s(X)) -> s#(p(q(X),d(X))) d#(s(X)) -> d#(X) d#(s(X)) -> s#(d(X)) d#(s(X)) -> s#(s(d(X))) p#(s(X),s(Y)) -> p#(X,Y) p#(s(X),s(Y)) -> s#(p(X,Y)) p#(s(X),s(Y)) -> s#(s(p(X,Y))) f#(s(X),cs(Y,Z)) -> a#(Z) a#(nt(X)) -> a#(X) a#(nt(X)) -> t#(a(X)) a#(ns(X)) -> a#(X) a#(ns(X)) -> s#(a(X)) a#(nf(X1,X2)) -> a#(X2) a#(nf(X1,X2)) -> a#(X1) a#(nf(X1,X2)) -> f#(a(X1),a(X2)) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X graph: a#(nf(X1,X2)) -> a#(X2) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2)) a#(nf(X1,X2)) -> a#(X2) -> a#(nf(X1,X2)) -> a#(X1) a#(nf(X1,X2)) -> a#(X2) -> a#(nf(X1,X2)) -> a#(X2) a#(nf(X1,X2)) -> a#(X2) -> a#(ns(X)) -> s#(a(X)) a#(nf(X1,X2)) -> a#(X2) -> a#(ns(X)) -> a#(X) a#(nf(X1,X2)) -> a#(X2) -> a#(nt(X)) -> t#(a(X)) a#(nf(X1,X2)) -> a#(X2) -> a#(nt(X)) -> a#(X) a#(nf(X1,X2)) -> a#(X1) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2)) a#(nf(X1,X2)) -> a#(X1) -> a#(nf(X1,X2)) -> a#(X1) a#(nf(X1,X2)) -> a#(X1) -> a#(nf(X1,X2)) -> a#(X2) a#(nf(X1,X2)) -> a#(X1) -> a#(ns(X)) -> s#(a(X)) a#(nf(X1,X2)) -> a#(X1) -> a#(ns(X)) -> a#(X) a#(nf(X1,X2)) -> a#(X1) -> a#(nt(X)) -> t#(a(X)) a#(nf(X1,X2)) -> a#(X1) -> a#(nt(X)) -> a#(X) a#(nf(X1,X2)) -> f#(a(X1),a(X2)) -> f#(s(X),cs(Y,Z)) -> a#(Z) a#(nt(X)) -> a#(X) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2)) a#(nt(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X1) a#(nt(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X2) a#(nt(X)) -> a#(X) -> a#(ns(X)) -> s#(a(X)) a#(nt(X)) -> a#(X) -> a#(ns(X)) -> a#(X) a#(nt(X)) -> a#(X) -> a#(nt(X)) -> t#(a(X)) a#(nt(X)) -> a#(X) -> a#(nt(X)) -> a#(X) a#(nt(X)) -> t#(a(X)) -> t#(N) -> q#(N) a#(ns(X)) -> a#(X) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2)) a#(ns(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X1) a#(ns(X)) -> a#(X) -> a#(nf(X1,X2)) -> a#(X2) a#(ns(X)) -> a#(X) -> a#(ns(X)) -> s#(a(X)) a#(ns(X)) -> a#(X) -> a#(ns(X)) -> a#(X) a#(ns(X)) -> a#(X) -> a#(nt(X)) -> t#(a(X)) a#(ns(X)) -> a#(X) -> a#(nt(X)) -> a#(X) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nf(X1,X2)) -> f#(a(X1),a(X2)) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nf(X1,X2)) -> a#(X1) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nf(X1,X2)) -> a#(X2) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(ns(X)) -> s#(a(X)) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(ns(X)) -> a#(X) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nt(X)) -> t#(a(X)) f#(s(X),cs(Y,Z)) -> a#(Z) -> a#(nt(X)) -> a#(X) p#(s(X),s(Y)) -> p#(X,Y) -> p#(s(X),s(Y)) -> s#(s(p(X,Y))) p#(s(X),s(Y)) -> p#(X,Y) -> p#(s(X),s(Y)) -> s#(p(X,Y)) p#(s(X),s(Y)) -> p#(X,Y) -> p#(s(X),s(Y)) -> p#(X,Y) d#(s(X)) -> d#(X) -> d#(s(X)) -> s#(s(d(X))) d#(s(X)) -> d#(X) -> d#(s(X)) -> s#(d(X)) d#(s(X)) -> d#(X) -> d#(s(X)) -> d#(X) q#(s(X)) -> p#(q(X),d(X)) -> p#(s(X),s(Y)) -> s#(s(p(X,Y))) q#(s(X)) -> p#(q(X),d(X)) -> p#(s(X),s(Y)) -> s#(p(X,Y)) q#(s(X)) -> p#(q(X),d(X)) -> p#(s(X),s(Y)) -> p#(X,Y) q#(s(X)) -> d#(X) -> d#(s(X)) -> s#(s(d(X))) q#(s(X)) -> d#(X) -> d#(s(X)) -> s#(d(X)) q#(s(X)) -> d#(X) -> d#(s(X)) -> d#(X) q#(s(X)) -> q#(X) -> q#(s(X)) -> s#(p(q(X),d(X))) q#(s(X)) -> q#(X) -> q#(s(X)) -> p#(q(X),d(X)) q#(s(X)) -> q#(X) -> q#(s(X)) -> q#(X) q#(s(X)) -> q#(X) -> q#(s(X)) -> d#(X) t#(N) -> q#(N) -> q#(s(X)) -> s#(p(q(X),d(X))) t#(N) -> q#(N) -> q#(s(X)) -> p#(q(X),d(X)) t#(N) -> q#(N) -> q#(s(X)) -> q#(X) t#(N) -> q#(N) -> q#(s(X)) -> d#(X) SCC Processor: #sccs: 4 #rules: 9 #arcs: 57/361 DPs: a#(nf(X1,X2)) -> a#(X2) a#(nt(X)) -> a#(X) a#(ns(X)) -> a#(X) a#(nf(X1,X2)) -> a#(X1) a#(nf(X1,X2)) -> f#(a(X1),a(X2)) f#(s(X),cs(Y,Z)) -> a#(Z) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [a#](x0) = x0 + 0, [f#](x0, x1) = x1, [nf](x0, x1) = x0 + x1, [a](x0) = x0 + 0, [nil] = 2, [f](x0, x1) = x0 + x1 + 0, [p](x0, x1) = x0 + x1 + 2, [d](x0) = x0 + 0, [s](x0) = x0 + 0, [0] = 5, [cs](x0, x1) = 1x0 + x1 + 0, [nt](x0) = 7x0 + 7, [ns](x0) = x0 + 0, [r](x0) = 3, [q](x0) = x0 + 5, [t](x0) = 7x0 + 7 orientation: a#(nf(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = a#(X2) a#(nt(X)) = 7X + 7 >= X + 0 = a#(X) a#(ns(X)) = X + 0 >= X + 0 = a#(X) a#(nf(X1,X2)) = X1 + X2 + 0 >= X1 + 0 = a#(X1) a#(nf(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = f#(a(X1),a(X2)) f#(s(X),cs(Y,Z)) = 1Y + Z + 0 >= Z + 0 = a#(Z) t(N) = 7N + 7 >= 7N + 7 = cs(r(q(N)),nt(ns(N))) q(0()) = 5 >= 5 = 0() q(s(X)) = X + 5 >= X + 5 = s(p(q(X),d(X))) d(0()) = 5 >= 5 = 0() d(s(X)) = X + 0 >= X + 0 = s(s(d(X))) p(0(),X) = X + 5 >= X = X p(X,0()) = X + 5 >= X = X p(s(X),s(Y)) = X + Y + 2 >= X + Y + 2 = s(s(p(X,Y))) f(0(),X) = X + 5 >= 2 = nil() f(s(X),cs(Y,Z)) = X + 1Y + Z + 0 >= X + 1Y + Z + 0 = cs(Y,nf(X,a(Z))) t(X) = 7X + 7 >= 7X + 7 = nt(X) s(X) = X + 0 >= X + 0 = ns(X) f(X1,X2) = X1 + X2 + 0 >= X1 + X2 = nf(X1,X2) a(nt(X)) = 7X + 7 >= 7X + 7 = t(a(X)) a(ns(X)) = X + 0 >= X + 0 = s(a(X)) a(nf(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = f(a(X1),a(X2)) a(X) = X + 0 >= X = X problem: DPs: a#(nf(X1,X2)) -> a#(X2) a#(ns(X)) -> a#(X) a#(nf(X1,X2)) -> a#(X1) a#(nf(X1,X2)) -> f#(a(X1),a(X2)) f#(s(X),cs(Y,Z)) -> a#(Z) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [a#](x0) = x0, [f#](x0, x1) = x0 + x1, [nf](x0, x1) = 4x0 + 4x1, [a](x0) = x0, [nil] = 0, [f](x0, x1) = 4x0 + 4x1, [p](x0, x1) = x0 + 1x1 + 0, [d](x0) = 0, [s](x0) = x0 + 0, [0] = 0, [cs](x0, x1) = x0 + x1, [nt](x0) = x0 + 4, [ns](x0) = x0 + 0, [r](x0) = 2, [q](x0) = 1, [t](x0) = x0 + 4 orientation: a#(nf(X1,X2)) = 4X1 + 4X2 >= X2 = a#(X2) a#(ns(X)) = X + 0 >= X = a#(X) a#(nf(X1,X2)) = 4X1 + 4X2 >= X1 = a#(X1) a#(nf(X1,X2)) = 4X1 + 4X2 >= X1 + X2 = f#(a(X1),a(X2)) f#(s(X),cs(Y,Z)) = X + Y + Z + 0 >= Z = a#(Z) t(N) = N + 4 >= N + 4 = cs(r(q(N)),nt(ns(N))) q(0()) = 1 >= 0 = 0() q(s(X)) = 1 >= 1 = s(p(q(X),d(X))) d(0()) = 0 >= 0 = 0() d(s(X)) = 0 >= 0 = s(s(d(X))) p(0(),X) = 1X + 0 >= X = X p(X,0()) = X + 1 >= X = X p(s(X),s(Y)) = X + 1Y + 1 >= X + 1Y + 0 = s(s(p(X,Y))) f(0(),X) = 4X + 4 >= 0 = nil() f(s(X),cs(Y,Z)) = 4X + 4Y + 4Z + 4 >= 4X + Y + 4Z = cs(Y,nf(X,a(Z))) t(X) = X + 4 >= X + 4 = nt(X) s(X) = X + 0 >= X + 0 = ns(X) f(X1,X2) = 4X1 + 4X2 >= 4X1 + 4X2 = nf(X1,X2) a(nt(X)) = X + 4 >= X + 4 = t(a(X)) a(ns(X)) = X + 0 >= X + 0 = s(a(X)) a(nf(X1,X2)) = 4X1 + 4X2 >= 4X1 + 4X2 = f(a(X1),a(X2)) a(X) = X >= X = X problem: DPs: a#(ns(X)) -> a#(X) f#(s(X),cs(Y,Z)) -> a#(Z) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X SCC Processor: #sccs: 1 #rules: 1 #arcs: 26/4 DPs: a#(ns(X)) -> a#(X) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Subterm Criterion Processor: simple projection: pi(a#) = 0 problem: DPs: TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Qed DPs: q#(s(X)) -> q#(X) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Subterm Criterion Processor: simple projection: pi(q#) = 0 problem: DPs: TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Qed DPs: p#(s(X),s(Y)) -> p#(X,Y) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Subterm Criterion Processor: simple projection: pi(p#) = 1 problem: DPs: TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Qed DPs: d#(s(X)) -> d#(X) TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Subterm Criterion Processor: simple projection: pi(d#) = 0 problem: DPs: TRS: t(N) -> cs(r(q(N)),nt(ns(N))) q(0()) -> 0() q(s(X)) -> s(p(q(X),d(X))) d(0()) -> 0() d(s(X)) -> s(s(d(X))) p(0(),X) -> X p(X,0()) -> X p(s(X),s(Y)) -> s(s(p(X,Y))) f(0(),X) -> nil() f(s(X),cs(Y,Z)) -> cs(Y,nf(X,a(Z))) t(X) -> nt(X) s(X) -> ns(X) f(X1,X2) -> nf(X1,X2) a(nt(X)) -> t(a(X)) a(ns(X)) -> s(a(X)) a(nf(X1,X2)) -> f(a(X1),a(X2)) a(X) -> X Qed