YES Problem: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) Proof: DP Processor: DPs: +#(*(x,y),*(x,z)) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u()) TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) EDG Processor: DPs: +#(*(x,y),*(x,z)) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u()) TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) graph: +#(+(x,y),z) -> +#(y,z) -> +#(*(x,y),*(x,z)) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u()) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u()) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) -> +#(*(x,y),*(x,z)) -> +#(y,z) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u()) +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(*(x,y),*(x,z)) -> +#(y,z) +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(*(x,y),*(x,z)) -> +#(y,z) -> +#(*(x,y),+(*(x,z),u())) -> +#(*(x,+(y,z)),u()) SCC Processor: #sccs: 1 #rules: 4 #arcs: 20/25 DPs: +#(+(x,y),z) -> +#(y,z) +#(*(x,y),+(*(x,z),u())) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) +#(*(x,y),*(x,z)) -> +#(y,z) TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) KBO Processor: argument filtering: pi(*) = [0,1] pi(+) = [0,1] pi(u) = [] pi(+#) = [0,1] weight function: w0 = 1 w(+#) = w(u) = w(*) = 1 w(+) = 0 precedence: +# ~ u ~ + ~ * problem: DPs: TRS: +(*(x,y),*(x,z)) -> *(x,+(y,z)) +(+(x,y),z) -> +(x,+(y,z)) +(*(x,y),+(*(x,z),u())) -> +(*(x,+(y,z)),u()) Qed