YES (VAR x) (RULES sqrt(0()) -> 0() +(0(),0()) -> 0() sqrt(+(i(x),x)) -> 0() i(0()) -> 0() ) (COMMENT Termination is shown by KBO with weight w0 = 1 w(i) = 1 w(0) = 1 w(sqrt) = 1 w(+) = 0 and precedence: i > sqrt > + > 0 )