YES Problem: f(x) -> s(x) f(s(s(x))) -> s(f(f(x))) Proof: DP Processor: DPs: f#(s(s(x))) -> f#(x) f#(s(s(x))) -> f#(f(x)) TRS: f(x) -> s(x) f(s(s(x))) -> s(f(f(x))) Matrix Interpretation Processor: dim=4 interpretation: [f#](x0) = [0 1 0 1]x0, [0 0 1 0] [1] [0 1 0 1] [0] [s](x0) = [0 0 0 0]x0 + [0] [1 0 0 0] [0], [0 0 1 0] [1] [0 1 0 1] [0] [f](x0) = [0 0 0 0]x0 + [0] [1 0 0 0] [0] orientation: f#(s(s(x))) = [1 1 1 1]x + [1] >= [0 1 0 1]x = f#(x) f#(s(s(x))) = [1 1 1 1]x + [1] >= [1 1 0 1]x = f#(f(x)) [0 0 1 0] [1] [0 0 1 0] [1] [0 1 0 1] [0] [0 1 0 1] [0] f(x) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = s(x) [1 0 0 0] [0] [1 0 0 0] [0] [0 0 0 0] [1] [0 0 0 0] [1] [1 1 1 1] [1] [1 1 1 1] [1] f(s(s(x))) = [0 0 0 0]x + [0] >= [0 0 0 0]x + [0] = s(f(f(x))) [0 0 0 0] [1] [0 0 0 0] [1] problem: DPs: TRS: f(x) -> s(x) f(s(s(x))) -> s(f(f(x))) Qed