YES TRS: merge(nil(),y) -> y merge(x,nil()) -> x merge(.(x,y),.(u,v)) -> if(<(x,u),.(x,merge(y,.(u,v))),.(u,merge(.(x,y),v))) ++(nil(),y) -> y ++(.(x,y),z) -> .(x,++(y,z)) if(true(),x,y) -> x if(false(),x,y) -> x max/plus interpretations on N: merge_A(x1,x2) = max{0, x1, x2} merge#_A(x1,x2) = max{0, x1, x2} nil_A = 0 nil#_A = 0 ._A(x1,x2) = max{0, x1, x2} .#_A(x1,x2) = max{0, x1, x2} if_A(x1,x2,x3) = max{0, x1, x2, x3} if#_A(x1,x2,x3) = max{0, x1, x2, x3} <_A(x1,x2) = max{0, x1, x2} <#_A(x1,x2) = max{0, x1, x2} ++_A(x1,x2) = max{0, x1, x2} ++#_A(x1,x2) = max{0, x1, x2} true_A = 0 true#_A = 0 false_A = 0 false#_A = 0 precedence: merge = nil = ++ = true = false > . = if = <