YES (VAR x) (RULES sqrt(0()) -> 0() +(0(),0()) -> 0() sqrt(+(i(x),x)) -> 0() i(0()) -> 0() ) (COMMENT Termination is shown by EKBO 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 weights w0 = 1 w(i) = 1 w(0) = 1 w(sqrt) = 1 w(+) = 0 and precedence: i > sqrt > + > 0 )