YES

Problem:
 a__c() -> a__f(g(c()))
 a__f(g(X)) -> g(X)
 mark(c()) -> a__c()
 mark(f(X)) -> a__f(X)
 mark(g(X)) -> g(X)
 a__c() -> c()
 a__f(X) -> f(X)

Proof:
 DP Processor:
  DPs:
   a__c#() -> a__f#(g(c()))
   mark#(c()) -> a__c#()
   mark#(f(X)) -> a__f#(X)
  TRS:
   a__c() -> a__f(g(c()))
   a__f(g(X)) -> g(X)
   mark(c()) -> a__c()
   mark(f(X)) -> a__f(X)
   mark(g(X)) -> g(X)
   a__c() -> c()
   a__f(X) -> f(X)
  Usable Rule Processor:
   DPs:
    a__c#() -> a__f#(g(c()))
    mark#(c()) -> a__c#()
    mark#(f(X)) -> a__f#(X)
   TRS:
    
   Arctic Interpretation Processor:
    dimension: 1
    usable rules:
     
    interpretation:
     [mark#](x0) = 2x0 + 5,
     
     [a__f#](x0) = x0 + 4,
     
     [a__c#] = 5,
     
     [f](x0) = x0 + 0,
     
     [g](x0) = x0 + 0,
     
     [c] = 4
    orientation:
     a__c#() = 5 >= 4 = a__f#(g(c()))
     
     mark#(c()) = 6 >= 5 = a__c#()
     
     mark#(f(X)) = 2X + 5 >= X + 4 = a__f#(X)
    problem:
     DPs:
      
     TRS:
      
    Qed