YES Problem: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) Proof: DP Processor: DPs: sqr#(s(x)) -> double#(x) sqr#(s(x)) -> sqr#(x) sqr#(s(x)) -> +#(sqr(x),s(double(x))) double#(s(x)) -> double#(x) +#(x,s(y)) -> +#(x,y) sqr#(s(x)) -> +#(sqr(x),double(x)) TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) TDG Processor: DPs: sqr#(s(x)) -> double#(x) sqr#(s(x)) -> sqr#(x) sqr#(s(x)) -> +#(sqr(x),s(double(x))) double#(s(x)) -> double#(x) +#(x,s(y)) -> +#(x,y) sqr#(s(x)) -> +#(sqr(x),double(x)) TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) graph: +#(x,s(y)) -> +#(x,y) -> +#(x,s(y)) -> +#(x,y) double#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x) sqr#(s(x)) -> +#(sqr(x),double(x)) -> +#(x,s(y)) -> +#(x,y) sqr#(s(x)) -> +#(sqr(x),s(double(x))) -> +#(x,s(y)) -> +#(x,y) sqr#(s(x)) -> double#(x) -> double#(s(x)) -> double#(x) sqr#(s(x)) -> sqr#(x) -> sqr#(s(x)) -> +#(sqr(x),double(x)) sqr#(s(x)) -> sqr#(x) -> sqr#(s(x)) -> +#(sqr(x),s(double(x))) sqr#(s(x)) -> sqr#(x) -> sqr#(s(x)) -> sqr#(x) sqr#(s(x)) -> sqr#(x) -> sqr#(s(x)) -> double#(x) SCC Processor: #sccs: 3 #rules: 3 #arcs: 9/36 DPs: sqr#(s(x)) -> sqr#(x) TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) LPO Processor: argument filtering: pi(0) = [] pi(sqr) = [0] pi(s) = [0] pi(double) = [0] pi(+) = [0,1] pi(sqr#) = 0 precedence: sqr > + ~ double > sqr# ~ s ~ 0 problem: DPs: TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) Qed DPs: double#(s(x)) -> double#(x) TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) LPO Processor: argument filtering: pi(0) = [] pi(sqr) = [0] pi(s) = [0] pi(double) = [0] pi(+) = [0,1] pi(double#) = 0 precedence: sqr > + ~ double > double# ~ s ~ 0 problem: DPs: TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) Qed DPs: +#(x,s(y)) -> +#(x,y) TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) LPO Processor: argument filtering: pi(0) = [] pi(sqr) = [0] pi(s) = [0] pi(double) = [0] pi(+) = [0,1] pi(+#) = 1 precedence: sqr > + ~ double > +# ~ s ~ 0 problem: DPs: TRS: sqr(0()) -> 0() sqr(s(x)) -> +(sqr(x),s(double(x))) double(0()) -> 0() double(s(x)) -> s(s(double(x))) +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) sqr(s(x)) -> s(+(sqr(x),double(x))) Qed