MAYBE
Trs:
 {                 fib(x) -> fibiter(x, 0(), 0(), s(0())),
            lt(0(), s(y)) -> true(),
           lt(s(x), s(y)) -> lt(x, y),
               lt(x, 0()) -> false(),
  if(false(), b, c, x, y) -> x,
   if(true(), b, c, x, y) -> fibiter(b, s(c), y, plus(x, y)),
             plus(0(), y) -> y,
            plus(s(x), y) -> s(plus(x, y)),
      fibiter(b, c, x, y) -> if(lt(c, b), b, c, x, y)}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open