YES
LCTRS
  Theories
    Core, Ints
  Signature
    f2: Int -> Int
    u_27: (Int, Int) -> Int
  Rules
    u_27(!n, !w_6) -> +(+(!n, -(!n, 1)), !w_6)
    f2(!n) -> u_27(!n, f2(-(!n, 2))) [>(!n, 1)]
    f2(!n) -> !n [<=(!n, 1)]
* DPGraph approximation on the DP problem
  dependency pairs:
    {f2#(!n) -> u_27#(!n, f2(-(!n, 2))) [>(!n, 1)]
    , f2#(!n) -> f2#(-(!n, 2)) [>(!n, 1)]}
  rules:
    {u_27(!n, !w_6) -> +(+(!n, -(!n, 1)), !w_6)
    , f2(!n) -> u_27(!n, f2(-(!n, 2))) [>(!n, 1)]
    , f2(!n) -> !n [<=(!n, 1)]}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: f2#(!n) -> u_27#(!n, f2(-(!n, 2))) [>(!n, 1)]
    , 2: f2#(!n) -> f2#(-(!n, 2)) [>(!n, 1)]}
  and edges
    1 -> {}
    2 -> {1, 2}
with 1 SCC(s)
  SCC:
    {f2#(!n) -> f2#(-(!n, 2)) [>(!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, 2)) [>(!n, 1)]}

Elapsed Time:  24.56 ms