YES LCTRS Theories Core, Ints Signature double: Int -> Int Rules double(!x) -> 0 [<=(!x, 0)] double(!x) -> +(2, double(-(!x, 1))) [>(!x, 0)] 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: 36.51 ms