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

Elapsed Time:  53.05 ms