YES Problem: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) Proof: DP Processor: DPs: +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(x,*(y,z)) sum#(cons(x,l)) -> sum#(l) sum#(cons(x,l)) -> +#(x,sum(l)) prod#(cons(x,l)) -> prod#(l) prod#(cons(x,l)) -> *#(x,prod(l)) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) TDG Processor: DPs: +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(x,*(y,z)) sum#(cons(x,l)) -> sum#(l) sum#(cons(x,l)) -> +#(x,sum(l)) prod#(cons(x,l)) -> prod#(l) prod#(cons(x,l)) -> *#(x,prod(l)) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) graph: prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> prod#(l) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(*(x,y),z) -> *#(x,*(y,z)) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(*(x,y),z) -> *#(y,z) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(s(x),s(y)) -> *#(x,y) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(s(x),s(y)) -> +#(x,y) sum#(cons(x,l)) -> sum#(l) -> sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> sum#(l) -> sum#(cons(x,l)) -> sum#(l) sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(+(x,y),z) -> +#(x,+(y,z)) sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(+(x,y),z) -> +#(y,z) sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(s(x),s(y)) -> +#(x,y) *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(x,*(y,z)) *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(y,z) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(y,z) -> *#(s(x),s(y)) -> *#(x,y) *#(*(x,y),z) -> *#(y,z) -> *#(s(x),s(y)) -> +#(x,y) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z)) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(s(x),s(y)) -> *#(x,y) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z)) *#(s(x),s(y)) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z) *#(s(x),s(y)) -> *#(x,y) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(s(x),s(y)) -> *#(x,y) -> *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> *#(x,y) -> *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) -> +#(+(x,y),z) -> +#(x,+(y,z)) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) -> +#(+(x,y),z) -> +#(y,z) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) -> +#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z)) *#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z) *#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> +#(x,y) +#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z) +#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(s(x),s(y)) -> +#(x,y) CDG Processor: DPs: +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(x,*(y,z)) sum#(cons(x,l)) -> sum#(l) sum#(cons(x,l)) -> +#(x,sum(l)) prod#(cons(x,l)) -> prod#(l) prod#(cons(x,l)) -> *#(x,prod(l)) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) graph: prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> prod#(l) prod#(cons(x,l)) -> prod#(l) -> prod#(cons(x,l)) -> *#(x,prod(l)) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(s(x),s(y)) -> +#(x,y) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(s(x),s(y)) -> *#(x,y) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(*(x,y),z) -> *#(y,z) prod#(cons(x,l)) -> *#(x,prod(l)) -> *#(*(x,y),z) -> *#(x,*(y,z)) sum#(cons(x,l)) -> sum#(l) -> sum#(cons(x,l)) -> sum#(l) sum#(cons(x,l)) -> sum#(l) -> sum#(cons(x,l)) -> +#(x,sum(l)) sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(s(x),s(y)) -> +#(x,y) sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(+(x,y),z) -> +#(y,z) sum#(cons(x,l)) -> +#(x,sum(l)) -> +#(+(x,y),z) -> +#(x,+(y,z)) *#(*(x,y),z) -> *#(y,z) -> *#(s(x),s(y)) -> +#(x,y) *#(*(x,y),z) -> *#(y,z) -> *#(s(x),s(y)) -> *#(x,y) *#(*(x,y),z) -> *#(y,z) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(y,z) -> *#(*(x,y),z) -> *#(x,*(y,z)) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(s(x),s(y)) -> +#(x,y) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(s(x),s(y)) -> *#(x,y) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(y,z) *#(*(x,y),z) -> *#(x,*(y,z)) -> *#(*(x,y),z) -> *#(x,*(y,z)) *#(s(x),s(y)) -> *#(x,y) -> *#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> *#(x,y) -> *#(s(x),s(y)) -> *#(x,y) *#(s(x),s(y)) -> *#(x,y) -> *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) *#(s(x),s(y)) -> *#(x,y) -> *#(*(x,y),z) -> *#(y,z) *#(s(x),s(y)) -> *#(x,y) -> *#(*(x,y),z) -> *#(x,*(y,z)) *#(s(x),s(y)) -> +#(*(x,y),+(x,y)) -> +#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> +#(x,y) *#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z) *#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(s(x),s(y)) -> +#(x,y) -> +#(s(x),s(y)) -> +#(x,y) +#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(y,z) +#(s(x),s(y)) -> +#(x,y) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) SCC Processor: #sccs: 4 #rules: 8 #arcs: 40/144 DPs: sum#(cons(x,l)) -> sum#(l) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) KBO Processor: argument filtering: pi(0) = [] pi(+) = [0,1] pi(s) = [] pi(*) = [0] pi(nil) = [] pi(sum) = 0 pi(cons) = [0,1] pi(prod) = 0 pi(sum#) = 0 weight function: w0 = 1 w(sum#) = w(prod) = w(sum) = w(nil) = w(s) = w(0) = 1 w(cons) = w(*) = w(+) = 0 precedence: sum# ~ cons ~ nil ~ * > prod ~ sum ~ s ~ + ~ 0 problem: DPs: TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) Qed DPs: prod#(cons(x,l)) -> prod#(l) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) KBO Processor: argument filtering: pi(0) = [] pi(+) = [0,1] pi(s) = [] pi(*) = [0] pi(nil) = [] pi(sum) = 0 pi(cons) = [0,1] pi(prod) = 0 pi(prod#) = 0 weight function: w0 = 1 w(prod#) = w(prod) = w(sum) = w(nil) = w(s) = w(0) = 1 w(cons) = w(*) = w(+) = 0 precedence: prod# ~ cons ~ nil ~ * > prod ~ sum ~ s ~ + ~ 0 problem: DPs: TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) Qed DPs: *#(*(x,y),z) -> *#(x,*(y,z)) *#(*(x,y),z) -> *#(y,z) *#(s(x),s(y)) -> *#(x,y) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) LPO Processor: argument filtering: pi(0) = [] pi(+) = [0,1] pi(s) = [0] pi(*) = [0,1] pi(nil) = [] pi(sum) = [0] pi(cons) = [0,1] pi(prod) = [0] pi(*#) = [0] precedence: prod > sum > * > + > s > *# ~ cons ~ nil ~ 0 problem: DPs: TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) Qed DPs: +#(s(x),s(y)) -> +#(x,y) +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) LPO Processor: argument filtering: pi(0) = [] pi(+) = [0,1] pi(s) = [0] pi(*) = [0,1] pi(nil) = [] pi(sum) = [0] pi(cons) = [0,1] pi(prod) = 0 pi(+#) = [0] precedence: nil > cons > * > sum > + > s > +# ~ prod ~ 0 problem: DPs: TRS: +(x,0()) -> x +(0(),x) -> x +(s(x),s(y)) -> s(s(+(x,y))) +(+(x,y),z) -> +(x,+(y,z)) *(x,0()) -> 0() *(0(),x) -> 0() *(s(x),s(y)) -> s(+(*(x,y),+(x,y))) *(*(x,y),z) -> *(x,*(y,z)) sum(nil()) -> 0() sum(cons(x,l)) -> +(x,sum(l)) prod(nil()) -> s(0()) prod(cons(x,l)) -> *(x,prod(l)) Qed