YES (VAR x) (RULES sqrt(0()) -> 0() +(0(),0()) -> 0() sqrt(+(i(x),x)) -> 0() i(0()) -> 0() ) (COMMENT Termination is shown by LPO with precedence: sqrt > + > i > 0 )