YES

(format LCTRS :logic QF_LIA)
(fun f1 1 :sort (Int Int))
(fun u_13 3 :sort (Int Int Int Int))

(rule (u_13 n_0 nx_1 w_4_2) (+ n_0 (+ nx_1 w_4_2)) :vars ((n_0 Int) (nx_1 Int) (w_4_2 Int)))
(rule (f1 n_3) (u_13 n_3 (- n_3 1) (f1 (- (- n_3 1) 1))) :guard (and (> n_3 1) (> (- n_3 1) 1)) :vars ((n_3 Int)))
(rule (f1 n_4) (+ n_4 (- n_4 1)) :guard (and (> n_4 1) (<= (- n_4 1) 1)) :vars ((n_4 Int)))
(rule (f1 n_5) n_5 :guard (<= n_5 1) :vars ((n_5 Int)))

Confluent by Orthogonality with proof:
no critical pairs

Elapsed Time:  33.44 ms