YES Problem: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) Proof: DP Processor: DPs: f#(x,c(y)) -> f#(y,y) f#(x,c(y)) -> f#(x,s(f(y,y))) f#(s(x),y) -> f#(x,s(c(y))) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) EDG Processor: DPs: f#(x,c(y)) -> f#(y,y) f#(x,c(y)) -> f#(x,s(f(y,y))) f#(s(x),y) -> f#(x,s(c(y))) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) graph: f#(s(x),y) -> f#(x,s(c(y))) -> f#(s(x),y) -> f#(x,s(c(y))) f#(x,c(y)) -> f#(y,y) -> f#(x,c(y)) -> f#(y,y) f#(x,c(y)) -> f#(y,y) -> f#(x,c(y)) -> f#(x,s(f(y,y))) f#(x,c(y)) -> f#(y,y) -> f#(s(x),y) -> f#(x,s(c(y))) f#(x,c(y)) -> f#(x,s(f(y,y))) -> f#(s(x),y) -> f#(x,s(c(y))) SCC Processor: #sccs: 2 #rules: 2 #arcs: 5/9 DPs: f#(x,c(y)) -> f#(y,y) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) KBO Processor: argument filtering: pi(c) = [0] pi(f) = [] pi(s) = [0] pi(f#) = 1 weight function: w0 = 1 w(f#) = w(s) = w(f) = w(c) = 1 precedence: f# ~ s ~ f ~ c problem: DPs: TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) Qed DPs: f#(s(x),y) -> f#(x,s(c(y))) TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) KBO Processor: argument filtering: pi(c) = [] pi(f) = [] pi(s) = [0] pi(f#) = [0,1] weight function: w0 = 1 w(f#) = w(f) = w(c) = 1 w(s) = 0 precedence: f# ~ s ~ f ~ c problem: DPs: TRS: f(x,c(y)) -> f(x,s(f(y,y))) f(s(x),y) -> f(x,s(c(y))) Qed