YES We show the termination of the TRS R: half(|0|()) -> |0|() half(s(|0|())) -> |0|() half(s(s(x))) -> s(half(x)) le(|0|(),y) -> true() le(s(x),|0|()) -> false() le(s(x),s(y)) -> le(x,y) inc(|0|()) -> |0|() inc(s(x)) -> s(inc(x)) log(x) -> log2(x,|0|()) log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) if(true(),x,s(y)) -> y if(false(),x,y) -> log2(half(x),y) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: half#(s(s(x))) -> half#(x) p2: le#(s(x),s(y)) -> le#(x,y) p3: inc#(s(x)) -> inc#(x) p4: log#(x) -> log2#(x,|0|()) p5: log2#(x,y) -> if#(le(x,s(|0|())),x,inc(y)) p6: log2#(x,y) -> le#(x,s(|0|())) p7: log2#(x,y) -> inc#(y) p8: if#(false(),x,y) -> log2#(half(x),y) p9: if#(false(),x,y) -> half#(x) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(|0|())) -> |0|() r3: half(s(s(x))) -> s(half(x)) r4: le(|0|(),y) -> true() r5: le(s(x),|0|()) -> false() r6: le(s(x),s(y)) -> le(x,y) r7: inc(|0|()) -> |0|() r8: inc(s(x)) -> s(inc(x)) r9: log(x) -> log2(x,|0|()) r10: log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) r11: if(true(),x,s(y)) -> y r12: if(false(),x,y) -> log2(half(x),y) The estimated dependency graph contains the following SCCs: {p5, p8} {p1} {p2} {p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: log2#(x,y) -> if#(le(x,s(|0|())),x,inc(y)) p2: if#(false(),x,y) -> log2#(half(x),y) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(|0|())) -> |0|() r3: half(s(s(x))) -> s(half(x)) r4: le(|0|(),y) -> true() r5: le(s(x),|0|()) -> false() r6: le(s(x),s(y)) -> le(x,y) r7: inc(|0|()) -> |0|() r8: inc(s(x)) -> s(inc(x)) r9: log(x) -> log2(x,|0|()) r10: log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) r11: if(true(),x,s(y)) -> y r12: if(false(),x,y) -> log2(half(x),y) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: log2#_A(x1,x2) = max{17, x1 - 12} if#_A(x1,x2,x3) = max{13, x1 + 1, x2 - 12} le_A(x1,x2) = max{0, x1 - 13} s_A(x1) = x1 + 31 |0|_A = 15 inc_A(x1) = x1 + 32 false_A = 17 half_A(x1) = max{24, x1 - 7} true_A = 1 precedence: half > log2# > if# > inc > le = s = |0| = false = true partial status: pi(log2#) = [] pi(if#) = [] pi(le) = [] pi(s) = [1] pi(|0|) = [] pi(inc) = [] pi(false) = [] pi(half) = [] pi(true) = [] 2. weighted path order base order: max/plus interpretations on natural numbers: log2#_A(x1,x2) = 39 if#_A(x1,x2,x3) = 39 le_A(x1,x2) = 42 s_A(x1) = 8 |0|_A = 7 inc_A(x1) = 8 false_A = 41 half_A(x1) = 14 true_A = 41 precedence: true > log2# > inc > s > if# = le = |0| > false > half partial status: pi(log2#) = [] pi(if#) = [] pi(le) = [] pi(s) = [] pi(|0|) = [] pi(inc) = [] pi(false) = [] pi(half) = [] pi(true) = [] The next rules are strictly ordered: p2 We remove them from the problem. -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: log2#(x,y) -> if#(le(x,s(|0|())),x,inc(y)) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(|0|())) -> |0|() r3: half(s(s(x))) -> s(half(x)) r4: le(|0|(),y) -> true() r5: le(s(x),|0|()) -> false() r6: le(s(x),s(y)) -> le(x,y) r7: inc(|0|()) -> |0|() r8: inc(s(x)) -> s(inc(x)) r9: log(x) -> log2(x,|0|()) r10: log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) r11: if(true(),x,s(y)) -> y r12: if(false(),x,y) -> log2(half(x),y) The estimated dependency graph contains the following SCCs: (no SCCs) -- 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(|0|())) -> |0|() r3: half(s(s(x))) -> s(half(x)) r4: le(|0|(),y) -> true() r5: le(s(x),|0|()) -> false() r6: le(s(x),s(y)) -> le(x,y) r7: inc(|0|()) -> |0|() r8: inc(s(x)) -> s(inc(x)) r9: log(x) -> log2(x,|0|()) r10: log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) r11: if(true(),x,s(y)) -> y r12: if(false(),x,y) -> log2(half(x),y) 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. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: le#(s(x),s(y)) -> le#(x,y) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(|0|())) -> |0|() r3: half(s(s(x))) -> s(half(x)) r4: le(|0|(),y) -> true() r5: le(s(x),|0|()) -> false() r6: le(s(x),s(y)) -> le(x,y) r7: inc(|0|()) -> |0|() r8: inc(s(x)) -> s(inc(x)) r9: log(x) -> log2(x,|0|()) r10: log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) r11: if(true(),x,s(y)) -> y r12: if(false(),x,y) -> log2(half(x),y) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: le#_A(x1,x2) = max{2, x1 - 1, x2 + 1} s_A(x1) = max{1, x1} precedence: le# = s partial status: pi(le#) = [2] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: le#_A(x1,x2) = 0 s_A(x1) = max{2, x1} precedence: le# = s partial status: pi(le#) = [] pi(s) = [1] 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: inc#(s(x)) -> inc#(x) and R consists of: r1: half(|0|()) -> |0|() r2: half(s(|0|())) -> |0|() r3: half(s(s(x))) -> s(half(x)) r4: le(|0|(),y) -> true() r5: le(s(x),|0|()) -> false() r6: le(s(x),s(y)) -> le(x,y) r7: inc(|0|()) -> |0|() r8: inc(s(x)) -> s(inc(x)) r9: log(x) -> log2(x,|0|()) r10: log2(x,y) -> if(le(x,s(|0|())),x,inc(y)) r11: if(true(),x,s(y)) -> y r12: if(false(),x,y) -> log2(half(x),y) The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: inc#_A(x1) = max{4, x1 + 3} s_A(x1) = max{3, x1 + 2} precedence: inc# = s partial status: pi(inc#) = [1] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: inc#_A(x1) = max{1, x1 - 1} s_A(x1) = x1 precedence: inc# = s partial status: pi(inc#) = [] pi(s) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.