YES We show the termination of the TRS R: cond(true(),x) -> cond(and(even(x),gr(x,|0|())),p(x)) and(x,false()) -> false() and(false(),x) -> false() and(true(),true()) -> true() even(|0|()) -> true() even(s(|0|())) -> false() even(s(s(x))) -> even(x) gr(|0|(),x) -> false() gr(s(x),|0|()) -> true() gr(s(x),s(y())) -> gr(x,y()) p(|0|()) -> |0|() p(s(x)) -> x -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: cond#(true(),x) -> cond#(and(even(x),gr(x,|0|())),p(x)) p2: cond#(true(),x) -> and#(even(x),gr(x,|0|())) p3: cond#(true(),x) -> even#(x) p4: cond#(true(),x) -> gr#(x,|0|()) p5: cond#(true(),x) -> p#(x) p6: even#(s(s(x))) -> even#(x) p7: gr#(s(x),s(y())) -> gr#(x,y()) and R consists of: r1: cond(true(),x) -> cond(and(even(x),gr(x,|0|())),p(x)) r2: and(x,false()) -> false() r3: and(false(),x) -> false() r4: and(true(),true()) -> true() r5: even(|0|()) -> true() r6: even(s(|0|())) -> false() r7: even(s(s(x))) -> even(x) r8: gr(|0|(),x) -> false() r9: gr(s(x),|0|()) -> true() r10: gr(s(x),s(y())) -> gr(x,y()) r11: p(|0|()) -> |0|() r12: p(s(x)) -> x The estimated dependency graph contains the following SCCs: {p1} {p6} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: cond#(true(),x) -> cond#(and(even(x),gr(x,|0|())),p(x)) and R consists of: r1: cond(true(),x) -> cond(and(even(x),gr(x,|0|())),p(x)) r2: and(x,false()) -> false() r3: and(false(),x) -> false() r4: and(true(),true()) -> true() r5: even(|0|()) -> true() r6: even(s(|0|())) -> false() r7: even(s(s(x))) -> even(x) r8: gr(|0|(),x) -> false() r9: gr(s(x),|0|()) -> true() r10: gr(s(x),s(y())) -> gr(x,y()) r11: p(|0|()) -> |0|() r12: p(s(x)) -> x The set of usable rules consists of r2, r3, r4, r5, r6, r7, r8, r9, r11, r12 Take the reduction pair: lexicographic combination of reduction pairs: 1. weighted path order base order: max/plus interpretations on natural numbers: cond#_A(x1,x2) = max{x1 + 3, x2 + 13} true_A = 18 and_A(x1,x2) = max{x1 - 11, x2 + 1} even_A(x1) = x1 + 13 gr_A(x1,x2) = max{16, x1 + 8, x2 + 1} |0|_A = 6 p_A(x1) = max{7, x1 - 1} false_A = 0 s_A(x1) = x1 + 19 precedence: cond# = true = and = even = p > gr = |0| = s > false partial status: pi(cond#) = [1, 2] pi(true) = [] pi(and) = [2] pi(even) = [1] pi(gr) = [1, 2] pi(|0|) = [] pi(p) = [] pi(false) = [] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: cond#_A(x1,x2) = max{1, x1 - 2, x2} true_A = 5 and_A(x1,x2) = x2 + 15 even_A(x1) = x1 + 13 gr_A(x1,x2) = max{x1 + 2, x2 + 15} |0|_A = 13 p_A(x1) = 12 false_A = 14 s_A(x1) = x1 + 6 precedence: cond# = true = and = even = gr = |0| = p = false = s partial status: pi(cond#) = [2] pi(true) = [] pi(and) = [2] pi(even) = [1] pi(gr) = [1, 2] pi(|0|) = [] pi(p) = [] pi(false) = [] 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: even#(s(s(x))) -> even#(x) and R consists of: r1: cond(true(),x) -> cond(and(even(x),gr(x,|0|())),p(x)) r2: and(x,false()) -> false() r3: and(false(),x) -> false() r4: and(true(),true()) -> true() r5: even(|0|()) -> true() r6: even(s(|0|())) -> false() r7: even(s(s(x))) -> even(x) r8: gr(|0|(),x) -> false() r9: gr(s(x),|0|()) -> true() r10: gr(s(x),s(y())) -> gr(x,y()) r11: p(|0|()) -> |0|() r12: p(s(x)) -> 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: even#_A(x1) = max{2, x1 + 1} s_A(x1) = max{1, x1} precedence: even# = s partial status: pi(even#) = [1] pi(s) = [1] 2. weighted path order base order: max/plus interpretations on natural numbers: even#_A(x1) = x1 + 1 s_A(x1) = x1 precedence: even# = s partial status: pi(even#) = [1] pi(s) = [1] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.