YES (VAR x) (RULES sqrt(0()) -> 0() +(0(),0()) -> 0() sqrt(+(i(x),x)) -> 0() i(0()) -> 0() ) (COMMENT Termination is shown by ELPO with interpretations on natural numbers i_A(x1) = 1 0_A = 1 sqrt_A(x1) = 1 +_A(x1,x2) = 1 0#_A = 0 +#_A(x1,x2) = x1 + x2 and precedence: + > sqrt > i > 0 )