YES

(format LCTRS :logic QF_LIA)
(fun double 1 :sort (Int Int))

(rule (double x_0) 0 :guard (<= x_0 0) :vars ((x_0 Int)))
(rule (double x_1) (+ 2 (double (- x_1 1))) :guard (> x_1 0) :vars ((x_1 Int)))

Confluent by Newmans Lemma with proof:
terminating and no critical pairs

Elapsed Time:  11.58 ms