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. lexicographic path order with precedence:
    
      precedence:
      
        d > a__g# > a__h# > c
      
      argument filter:
    
        pi(a__g#) = [1]
        pi(a__h#) = [1]
        pi(d) = []
        pi(c) = []
    
    2. lexicographic path order with precedence:
    
      precedence:
      
        c > a__g# > d > a__h#
      
      argument filter:
    
        pi(a__g#) = [1]
        pi(a__h#) = [1]
        pi(d) = []
        pi(c) = []
    
    3. lexicographic path order with precedence:
    
      precedence:
      
        c > a__g# > d > a__h#
      
      argument filter:
    
        pi(a__g#) = [1]
        pi(a__h#) = 1
        pi(d) = []
        pi(c) = []
    

The next rules are strictly ordered:

  p1, p2
  r1, r2, r3, r4, r5, r6, r7, r8, r9, r10

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