YES Problem: +(x,0()) -> x +(x,s(y)) -> s(+(x,y)) d(0()) -> 0() d(s(x)) -> s(s(d(x))) f(0()) -> 0() f(s(x)) -> +(+(s(x),s(x)),s(x)) f(g(0())) -> +(+(g(0()),g(0())),g(0())) g(x) -> s(d(x)) Proof: Church Rosser Transformation Processor: f(s(x104)) -> +(+(s(x104),s(x104)),s(x104)) g(0()) -> s(d(0())) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = 7x0, [+](x0, x1) = 2x0 + x1, [d](x0) = 2x0, [g](x0) = 6x0 + 3, [0] = 2, [s](x0) = 2x0 orientation: f(s(x104)) = 14x104 >= 14x104 = +(+(s(x104),s(x104)),s(x104)) g(0()) = 15 >= 8 = s(d(0())) problem: f(s(x104)) -> +(+(s(x104),s(x104)),s(x104)) Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = 7x0 + 7, [+](x0, x1) = x0 + 2x1 + 5, [s](x0) = 2x0 + 3 orientation: f(s(x104)) = 14x104 + 28 >= 10x104 + 25 = +(+(s(x104),s(x104)),s(x104)) problem: Qed