YES
LCTRS
  Theories
    Core, Ints
  Signature
    double: Int -> Int
  Rules
    double(!x) -> 0 [<=(!x, 0)]
    double(!x) -> +(2, double(-(!x, 1))) [>(!x, 0)]
* DPGraph approximation on the DP problem
  dependency pairs:
    {double#(!x) -> double#(-(!x, 1)) [>(!x, 0)]}
  rules:
    {double(!x) -> 0 [<=(!x, 0)]
    , double(!x) -> +(2, double(-(!x, 1))) [>(!x, 0)]}
resulting in the DP graph
  DPGraph with indexed dependency pairs
    {1: double#(!x) -> double#(-(!x, 1)) [>(!x, 0)]}
  and edges
    1 -> {1}
with 1 SCC(s)
  SCC:
    {double#(!x) -> double#(-(!x, 1)) [>(!x, 0)]}
* Value criterion after 1 iteration(s) with the projections:
  Iteration 1:
    projection(s):
      v(double#) = 1
    removing the rule(s):
      {double#(!x) -> double#(-(!x, 1)) [>(!x, 0)]}

Elapsed Time:  22.52 ms