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{3, 2, 2} or#_A(x1,x2) = max{5, 1, 3} true_A = 3 true#_A = 0 false_A = 3 false#_A = 4 mem_A(x1,x2) = max{3, -1, 1} mem#_A(x1,x2) = max{5, 2 + x1, 3} nil_A = 1 nil#_A = 5 set_A(x1) = max{1, 1 + x1} set#_A(x1) = max{0, 0} =_A(x1,x2) = max{2, 2, -1} =#_A(x1,x2) = max{0, 0, 0} union_A(x1,x2) = max{1, 1 + x1, 1 + x2} union#_A(x1,x2) = max{0, 0, 0} precedence: mem > or = nil = set = = = union > true = false