YES

Problem:
 0(x1) -> 1(x1)
 4(5(4(5(x1)))) -> 4(4(5(5(x1))))
 5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) -> 2(x1)

Proof:
 DP Processor:
  DPs:
   4#(5(4(5(x1)))) -> 5#(5(x1))
   4#(5(4(5(x1)))) -> 4#(5(5(x1)))
   4#(5(4(5(x1)))) -> 4#(4(5(5(x1))))
  TRS:
   0(x1) -> 1(x1)
   4(5(4(5(x1)))) -> 4(4(5(5(x1))))
   5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) -> 2(x1)
  Usable Rule Processor:
   DPs:
    4#(5(4(5(x1)))) -> 5#(5(x1))
    4#(5(4(5(x1)))) -> 4#(5(5(x1)))
    4#(5(4(5(x1)))) -> 4#(4(5(5(x1))))
   TRS:
    5(5(5(5(5(5(4(4(4(4(4(4(x1)))))))))))) -> 2(x1)
    4(5(4(5(x1)))) -> 4(4(5(5(x1))))
   KBO Processor:
    weight function:
     w0 = 1
     w(5#) = w(2) = w(4) = w(5) = 1
     w(4#) = 0
    precedence:
     4# > 5 > 5# ~ 2 ~ 4
    problem:
     DPs:
      
     TRS:
      
    Qed