YES Problem: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Proof: DP Processor: DPs: half#(s(s(x))) -> half#(x) log#(s(s(x))) -> half#(x) log#(s(s(x))) -> log#(s(half(x))) TRS: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Matrix Interpretation Processor: dim=1 interpretation: [log#](x0) = 6x0 + 4, [half#](x0) = x0, [log](x0) = x0, [s](x0) = 2x0 + 1, [half](x0) = x0, [0] = 0 orientation: half#(s(s(x))) = 4x + 3 >= x = half#(x) log#(s(s(x))) = 24x + 22 >= x = half#(x) log#(s(s(x))) = 24x + 22 >= 12x + 10 = log#(s(half(x))) half(0()) = 0 >= 0 = 0() half(s(s(x))) = 4x + 3 >= 2x + 1 = s(half(x)) log(s(0())) = 1 >= 0 = 0() log(s(s(x))) = 4x + 3 >= 4x + 3 = s(log(s(half(x)))) problem: DPs: TRS: half(0()) -> 0() half(s(s(x))) -> s(half(x)) log(s(0())) -> 0() log(s(s(x))) -> s(log(s(half(x)))) Qed