YES We show the termination of the TRS R: half(|0|()) -> |0|() half(s(s(x))) -> s(half(x)) log(s(|0|())) -> |0|() log(s(s(x))) -> s(log(s(half(x)))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: half#(s(s(x))) -> half#(x) p2: log#(s(s(x))) -> log#(s(half(x))) p3: log#(s(s(x))) -> half#(x) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(s(x))) -> s(half(x)) r3: log(s(|0|())) -> |0|() r4: log(s(s(x))) -> s(log(s(half(x)))) The estimated dependency graph contains the following SCCs: {p2} {p1} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: log#(s(s(x))) -> log#(s(half(x))) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(s(x))) -> s(half(x)) r3: log(s(|0|())) -> |0|() r4: log(s(s(x))) -> s(log(s(half(x)))) The set of usable rules consists of r1, r2 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: log#_A(x1) = x1 + 9 s_A(x1) = x1 + 4 half_A(x1) = x1 + 3 |0|_A = 2 precedence: log# = s = half = |0| partial status: pi(log#) = [] pi(s) = [] pi(half) = [] pi(|0|) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: log#_A(x1) = x1 + 5 s_A(x1) = x1 + 2 half_A(x1) = max{2, x1} |0|_A = 3 precedence: log# = s = half = |0| partial status: pi(log#) = [] pi(s) = [1] pi(half) = [1] pi(|0|) = [] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: half#(s(s(x))) -> half#(x) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(s(x))) -> s(half(x)) r3: log(s(|0|())) -> |0|() r4: log(s(s(x))) -> s(log(s(half(x)))) The set of usable rules consists of (no rules) Take the monotone reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: half#_A(x1) = max{2, x1 + 1} s_A(x1) = max{1, x1} precedence: half# = s partial status: pi(half#) = [1] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: half#_A(x1) = x1 + 1 s_A(x1) = x1 precedence: half# = s partial status: pi(half#) = [1] pi(s) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.