YES LCTRS Theories Core, Ints Signature double: Int -> Int Rules double(?7) -> +(2, double(-(?7, 1))) [>(?7, 0)] double(?8) -> 0 [<=(?8, 0)] Confluent by Strong Closedness with proof: no critical pairs Elapsed Time: 29.96 ms