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 approximation on the DP problem
  dependency pairs:
    {f2#(!n) -> u_15#(!n, f2(-(!n, 1))) [>(!n, 1)]
    , f2#(!n) -> f2#(-(!n, 1)) [>(!n, 1)]}
  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)]}
resulting in the DP graph
  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:  21.99 ms