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:

  matrix interpretations:
  
    carrier: N^1
    order: standard order
    interpretations:
      a__g#_A(x1) = x1
      a__h#_A(x1) = x1
      d_A() = 2
      c_A() = 1

The next rules are strictly ordered:

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

We remove them from the problem.

-- SCC decomposition.

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

p1: a__g#(X) -> a__h#(X)

and R consists of:

  (no rules)

The estimated dependency graph contains the following SCCs:

  (no SCCs)