YES We show the termination of the TRS R: admit(x,nil()) -> nil() admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) cond(true(),y) -> y -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: admit#(x,.(u,.(v,.(w(),z)))) -> cond#(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) p2: admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z) and R consists of: r1: admit(x,nil()) -> nil() r2: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) r3: cond(true(),y) -> y The estimated dependency graph contains the following SCCs: {p2} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: admit#(x,.(u,.(v,.(w(),z)))) -> admit#(carry(x,u,v),z) and R consists of: r1: admit(x,nil()) -> nil() r2: admit(x,.(u,.(v,.(w(),z)))) -> cond(=(sum(x,u,v),w()),.(u,.(v,.(w(),admit(carry(x,u,v),z))))) r3: cond(true(),y) -> y The set of usable rules consists of (no rules) Take the reduction pair: lexicographic combination of reduction pairs: 1. matrix interpretations: carrier: N^1 order: standard order interpretations: admit#_A(x1,x2) = x2 ._A(x1,x2) = x1 + x2 w_A() = 1 carry_A(x1,x2,x3) = x2 + x3 + 1 2. lexicographic path order with precedence: precedence: . > carry > admit# > w argument filter: pi(admit#) = 2 pi(.) = [1, 2] pi(w) = [] pi(carry) = [2, 3] The next rules are strictly ordered: p1 We remove them from the problem. Then no dependency pair remains.