YES
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:
  Strict:
   {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)}
  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))}
  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#(h(X)) -> mark#(X), mark#(c(X)) -> a__c#(X))
    (mark#(h(X)) -> mark#(X), mark#(h(X)) -> a__h#(mark(X)))
    (mark#(h(X)) -> mark#(X), mark#(h(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))
    (mark#(f(X)) -> mark#(X), mark#(c(X)) -> a__c#(X))
    (mark#(f(X)) -> mark#(X), mark#(h(X)) -> a__h#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(h(X)) -> mark#(X))}
   SCCS:
    Scc:
     {mark#(f(X)) -> mark#(X),
      mark#(h(X)) -> mark#(X)}
    SCC:
     Strict:
      {mark#(f(X)) -> mark#(X),
       mark#(h(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))}
     SPSC:
      Simple Projection:
       pi(mark#) = 0
      Strict:
       {mark#(h(X)) -> mark#(X)}
      EDG:
       {(mark#(h(X)) -> mark#(X), mark#(h(X)) -> mark#(X))}
       SCCS:
        Scc:
         {mark#(h(X)) -> mark#(X)}
        SCC:
         Strict:
          {mark#(h(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))}
         SPSC:
          Simple Projection:
           pi(mark#) = 0
          Strict:
           {}
          Qed