YES Problem: b(x,y) -> c(a(c(y),a(0(),x))) a(y,x) -> y a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0()) Proof: DP Processor: DPs: b#(x,y) -> a#(0(),x) b#(x,y) -> a#(c(y),a(0(),x)) a#(y,c(b(a(0(),x),0()))) -> b#(0(),y) a#(y,c(b(a(0(),x),0()))) -> a#(c(b(0(),y)),x) a#(y,c(b(a(0(),x),0()))) -> b#(a(c(b(0(),y)),x),0()) TRS: b(x,y) -> c(a(c(y),a(0(),x))) a(y,x) -> y a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0()) Matrix Interpretation Processor: dim=2 interpretation: [a#](x0, x1) = [1 0]x1, [b#](x0, x1) = [1 0]x0 + [1], [1 0] [0 0] [a](x0, x1) = [0 2]x0 + [1 0]x1, [0] [0] = [1], [0 2] [c](x0) = [0 0]x0, [0 0] [0] [b](x0, x1) = [0 1]x0 + [1] orientation: b#(x,y) = [1 0]x + [1] >= [1 0]x = a#(0(),x) b#(x,y) = [1 0]x + [1] >= [0] = a#(c(y),a(0(),x)) a#(y,c(b(a(0(),x),0()))) = [2 0]x + [6] >= [1] = b#(0(),y) a#(y,c(b(a(0(),x),0()))) = [2 0]x + [6] >= [1 0]x = a#(c(b(0(),y)),x) a#(y,c(b(a(0(),x),0()))) = [2 0]x + [6] >= [5] = b#(a(c(b(0(),y)),x),0()) [0 0] [0] [0] b(x,y) = [0 1]x + [1] >= [0] = c(a(c(y),a(0(),x))) [0 0] [1 0] a(y,x) = [1 0]x + [0 2]y >= y = y [0 0] [1 0] [0] [0 0] [0] a(y,c(b(a(0(),x),0()))) = [2 0]x + [0 2]y + [6] >= [1 0]x + [1] = b(a(c(b(0(),y)),x),0()) problem: DPs: TRS: b(x,y) -> c(a(c(y),a(0(),x))) a(y,x) -> y a(y,c(b(a(0(),x),0()))) -> b(a(c(b(0(),y)),x),0()) Qed