YES TRS: or(true(),y) -> true() or(x,true()) -> true() or(false(),false()) -> false() mem(x,nil()) -> false() mem(x,set(y)) -> =(x,y) mem(x,union(y,z)) -> or(mem(x,y),mem(x,z)) max/plus interpretations on N: or_A(x1,x2) = max{2, x1, x2} or#_A(x1,x2) = max{2, x1, x2} true_A = 0 true#_A = 0 false_A = 0 false#_A = 0 mem_A(x1,x2) = max{2, 1 + x1, x2} mem#_A(x1,x2) = max{2, 1 + x1, x2} nil_A = 1 nil#_A = 1 set_A(x1) = max{1, 1 + x1} set#_A(x1) = max{1, 1 + x1} =_A(x1,x2) = max{0, x1, x2} =#_A(x1,x2) = max{0, x1, x2} union_A(x1,x2) = max{0, x1, x2} union#_A(x1,x2) = max{0, x1, x2} precedence: nil > false > true = mem = set = union > or = =