YES
LCTRS
  Theories
    Core, Ints
  Sorts
    Unit
  Signature
    fastfib: Int -> Unit
    return: Int -> Unit
    u: (Int, Int, Int, Int, Int) -> Unit
    v: (Int, Int, Int, Int, Int) -> Unit
  Rules
    v(!n, !pre1, !pre2, !val, !i) -> return(!val) [and(not(<=(!i, !n)), not(<(!val, 0)))]
    v(!n, !pre1, !pre2, !val, !i) -> return(-1) [and(not(<=(!i, !n)), <(!val, 0))]
    v(!n, !pre1, !pre2, !val, !i) -> v(!n, +(!pre1, !pre2), !pre1, +(!pre1, !pre2), +(!i, 1)) [<=(!i, !n)]
    u(!n, !pre1, !pre2, !val, !i) -> v(!n, !pre1, !pre2, !val, 2) [and(not(<=(!n, 0)), not(!n = 1))]
    u(!n, !pre1, !pre2, !val, !i) -> return(1) [and(not(<=(!n, 0)), !n = 1)]
    u(!n, !pre1, !pre2, !val, !i) -> return(0) [<=(!n, 0)]
    fastfib(!n) -> u(!n, 1, 0, 0, !rnd)
* DPGraph approximation on the DP problem
  dependency pairs:
    {v#(!n, !pre1, !pre2, !val, !i) -> v#(!n, +(!pre1, !pre2), !pre1, +(!pre1, !pre2), +(!i, 1)) [<=(!i, !n)]
    , u#(!n, !pre1, !pre2, !val, !i) -> v#(!n, !pre1, !pre2, !val, 2) [and(not(<=(!n, 0)), not(=(!n, 1)))]
    , fastfib#(!n) -> u#(!n, 1, 0, 0, !rnd)}
  rules:
    {v(!n, !pre1, !pre2, !val, !i) -> return(!val) [and(not(<=(!i, !n)), not(<(!val, 0)))]
    , v(!n, !pre1, !pre2, !val, !i) -> return(-1) [and(not(<=(!i, !n)), <(!val, 0))]
    , v(!n, !pre1, !pre2, !val, !i) -> v(!n, +(!pre1, !pre2), !pre1, +(!pre1, !pre2), +(!i, 1)) [<=(!i, !n)]
    , u(!n, !pre1, !pre2, !val, !i) -> v(!n, !pre1, !pre2, !val, 2) [and(not(<=(!n, 0)), not(=(!n, 1)))]
    , u(!n, !pre1, !pre2, !val, !i) -> return(1) [and(not(<=(!n, 0)), =(!n, 1))]
    , u(!n, !pre1, !pre2, !val, !i) -> return(0) [<=(!n, 0)]
    , fastfib(!n) -> u(!n, 1, 0, 0, !rnd)}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: v#(!n, !pre1, !pre2, !val, !i) -> v#(!n, +(!pre1, !pre2), !pre1, +(!pre1, !pre2), +(!i, 1)) [<=(!i, !n)]
    , 2: u#(!n, !pre1, !pre2, !val, !i) -> v#(!n, !pre1, !pre2, !val, 2) [and(not(<=(!n, 0)), not(=(!n, 1)))]
    , 3: fastfib#(!n) -> u#(!n, 1, 0, 0, !rnd)}
  and edges
    1 -> {1}
    2 -> {1}
    3 -> {2}
with 1 SCC(s)
  SCC:
    {v#(!n, !pre1, !pre2, !val, !i) -> v#(!n, +(!pre1, !pre2), !pre1, +(!pre1, !pre2), +(!i, 1)) [<=(!i, !n)]}
* Value criterion after 1 iteration(s) with the linear poly projections:
  Iteration 1:
    projection(s):
      v(v#(x1, x2, x3, x4, x5)) = x1 + -1 * x5
    removing the rule(s):
      {v#(!n, !pre1, !pre2, !val, !i) -> v#(!n, +(!pre1, !pre2), !pre1, +(!pre1, !pre2), +(!i, 1)) [<=(!i, !n)]}

Elapsed Time:  49.33 ms