YES (VAR x0 x1 x) (RULES f(x0,nil()) -> nil() g(x0,x1) -> x0 cdr(nil()) -> nil() cons(x,nil()) -> x ) (COMMENT Termination is shown by LPO with precedence: cdr > g > cons > f > nil )