YES

We show the termination of the TRS R:

  a__g(X) -> a__h(X)
  a__c() -> d()
  a__h(d()) -> a__g(c())
  mark(g(X)) -> a__g(X)
  mark(h(X)) -> a__h(X)
  mark(c()) -> a__c()
  mark(d()) -> d()
  a__g(X) -> g(X)
  a__h(X) -> h(X)
  a__c() -> c()

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: a__g#(X) -> a__h#(X)
p2: a__h#(d()) -> a__g#(c())
p3: mark#(g(X)) -> a__g#(X)
p4: mark#(h(X)) -> a__h#(X)
p5: mark#(c()) -> a__c#()

and R consists of:

r1: a__g(X) -> a__h(X)
r2: a__c() -> d()
r3: a__h(d()) -> a__g(c())
r4: mark(g(X)) -> a__g(X)
r5: mark(h(X)) -> a__h(X)
r6: mark(c()) -> a__c()
r7: mark(d()) -> d()
r8: a__g(X) -> g(X)
r9: a__h(X) -> h(X)
r10: a__c() -> c()

The estimated dependency graph contains the following SCCs:

  {p1, p2}


-- Reduction pair.

Consider the dependency pair problem (P, R), where P consists of

p1: a__g#(X) -> a__h#(X)
p2: a__h#(d()) -> a__g#(c())

and R consists of:

r1: a__g(X) -> a__h(X)
r2: a__c() -> d()
r3: a__h(d()) -> a__g(c())
r4: mark(g(X)) -> a__g(X)
r5: mark(h(X)) -> a__h(X)
r6: mark(c()) -> a__c()
r7: mark(d()) -> d()
r8: a__g(X) -> g(X)
r9: a__h(X) -> h(X)
r10: a__c() -> c()

The set of usable rules consists of

  (no rules)

Take the monotone reduction pair:

  lexicographic combination of reduction pairs:
  
    1. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__g#_A(x1) = max{7, x1 + 2}
          a__h#_A(x1) = max{3, x1 + 2}
          d_A = 5
          c_A = 4
    
      precedence:
      
        a__g# = a__h# = d = c
      
      partial status:
    
        pi(a__g#) = [1]
        pi(a__h#) = [1]
        pi(d) = []
        pi(c) = []
    
    2. weighted path order
    
      base order:
    
        max/plus interpretations on natural numbers:
        
          a__g#_A(x1) = max{4, x1 + 2}
          a__h#_A(x1) = max{1, x1}
          d_A = 3
          c_A = 2
    
      precedence:
      
        a__g# = a__h# = d = c
      
      partial status:
    
        pi(a__g#) = [1]
        pi(a__h#) = [1]
        pi(d) = []
        pi(c) = []
    

The next rules are strictly ordered:

  p1, p2

We remove them from the problem.  Then no dependency pair remains.