YES
Time: 0.017328
TRS:
 {  a__c X -> d X,
    a__c X -> c X,
    a__f X -> f X,
  a__f f X -> a__c f g f X,
    a__h X -> a__c d X,
    a__h X -> h X,
  mark f X -> a__f mark X,
  mark g X -> g X,
  mark d X -> d X,
  mark c X -> a__c X,
  mark h X -> a__h mark X}
 DP:
  DP:
   {a__f# f X -> a__c# f g f X,
      a__h# X -> a__c# d X,
    mark# f X -> a__f# mark X,
    mark# f X -> mark# X,
    mark# c X -> a__c# X,
    mark# h X -> a__h# mark X,
    mark# h X -> mark# X}
  TRS:
  {  a__c X -> d X,
     a__c X -> c X,
     a__f X -> f X,
   a__f f X -> a__c f g f X,
     a__h X -> a__c d X,
     a__h X -> h X,
   mark f X -> a__f mark X,
   mark g X -> g X,
   mark d X -> d X,
   mark c X -> a__c X,
   mark h X -> a__h mark X}
  EDG:
   {(mark# h X -> a__h# mark X, a__h# X -> a__c# d X)
    (mark# f X -> a__f# mark X, a__f# f X -> a__c# f g f X)
    (mark# h X -> mark# X, mark# f X -> a__f# mark X)
    (mark# h X -> mark# X, mark# f X -> mark# X)
    (mark# f X -> mark# X, mark# f X -> a__f# mark X)
    (mark# f X -> mark# X, mark# f X -> mark# X)}
   STATUS:
    arrows: 0.877551
    SCCS (1):
     Scc:
      {mark# f X -> mark# X}
     
     
     
     
     
     SCC (1):
      Strict:
       {mark# f X -> mark# X}
      Weak:
      {  a__c X -> d X,
         a__c X -> c X,
         a__f X -> f X,
       a__f f X -> a__c f g f X,
         a__h X -> a__c d X,
         a__h X -> h X,
       mark f X -> a__f mark X,
       mark g X -> g X,
       mark d X -> d X,
       mark c X -> a__c X,
       mark h X -> a__h mark X}
      POLY:
       Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
       Interpretation:
        [a__c](x0) = x0,
        
        [f](x0) = x0 + 1,
        
        [g](x0) = 1,
        
        [a__f](x0) = x0 + 1,
        
        [d](x0) = 0,
        
        [a__h](x0) = x0 + 1,
        
        [mark](x0) = x0 + 1,
        
        [c](x0) = 1,
        
        [h](x0) = 1,
        
        [mark#](x0) = x0 + 1
       Strict:
        mark# f X -> mark# X
        2 + 1X >= 1 + 1X
       Weak:
        mark h X -> a__h mark X
        2 + 0X >= 2 + 1X
        mark c X -> a__c X
        2 + 0X >= 0 + 1X
        mark d X -> d X
        1 + 0X >= 0 + 0X
        mark g X -> g X
        2 + 0X >= 1 + 0X
        mark f X -> a__f mark X
        2 + 1X >= 2 + 1X
        a__h X -> h X
        1 + 1X >= 1 + 0X
        a__h X -> a__c d X
        1 + 1X >= 0 + 0X
        a__f f X -> a__c f g f X
        2 + 1X >= 2 + 0X
        a__f X -> f X
        1 + 1X >= 1 + 1X
        a__c X -> c X
        0 + 1X >= 1 + 0X
        a__c X -> d X
        0 + 1X >= 0 + 0X
      Qed