YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fib: Int -> Unit
    return: Int -> Unit
    w: (Unit, Unit) -> Unit
  Rules
    w(return(!x), return(!y)) -> return(+(!x, !y))
    fib(!x) -> w(fib(-(!x, 1)), fib(-(!x, 2))) [>=(-(!x, 2), 0)]
    fib(1) -> return(1)
    fib(!x) -> return(0) [<=(!x, 0)]
DPGraph with indexed dependency pairs
  {1: fib#(!x) -> w#(fib(-(!x, 1)), fib(-(!x, 2))) [>=(-(!x, 2), 0)]
  , 2: fib#(!x) -> fib#(-(!x, 1)) [>=(-(!x, 2), 0)]
  , 3: fib#(!x) -> fib#(-(!x, 2)) [>=(-(!x, 2), 0)]}
and edges
  1 -> {}
  2 -> {1, 2, 3}
  3 -> {1, 2, 3}
with 1 SCC(s)
  SCC:
    {fib#(!x) -> fib#(-(!x, 2)) [>=(-(!x, 2), 0)]
    , fib#(!x) -> fib#(-(!x, 1)) [>=(-(!x, 2), 0)]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(fib#) = 1
    removing the rule(s):
      {fib#(!x) -> fib#(-(!x, 2)) [>=(-(!x, 2), 0)]
      , fib#(!x) -> fib#(-(!x, 1)) [>=(-(!x, 2), 0)]}

Elapsed Time:  35.39 ms