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

Elapsed Time:  36.62 ms