YES

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

(rule (double n_0) (u n_0 1 0) :vars ((n_0 Int)))
(rule (u n_1 i_2 z_3) (u n_1 (+ i_2 1) (sucsuc z_3)) :guard (<= i_2 n_1) :vars ((n_1 Int) (i_2 Int) (z_3 Int)))
(rule (u n_4 i_5 z_6) z_6 :guard (not (<= i_5 n_4)) :vars ((n_4 Int) (i_5 Int) (z_6 Int)))
(rule (sucsuc x_7) (+ x_7 2) :vars ((x_7 Int)))

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

Elapsed Time:  12.32 ms