YES
LCTRS
  Theories
    Core, Ints
  Signature
    f2: Int -> Int
    u_15: (Int, Int) -> Int
  Rules
    u_15(!n, !w_4) -> +(!n, !w_4) [distinct(!n, 10)]
    u_15(!n, !w_4) -> 10 [!n = 10]
    f2(!n) -> u_15(!n, f2(-(!n, 1))) [>(!n, 1)]
    f2(!n) -> !n [<=(!n, 1)]
DPGraph with indexed dependency pairs
  {1: f2#(!n) -> u_15#(!n, f2(-(!n, 1))) [>(!n, 1)]
  , 2: f2#(!n) -> f2#(-(!n, 1)) [>(!n, 1)]}
and edges
  1 -> {}
  2 -> {1, 2}
with 1 SCC(s)
  SCC:
    {f2#(!n) -> f2#(-(!n, 1)) [>(!n, 1)]}
Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(f2#) = 1
    removing the rule(s):
      {f2#(!n) -> f2#(-(!n, 1)) [>(!n, 1)]}

Elapsed Time:  31.47 ms