YES
TRS:
 {       mark(f(X)) -> active(f(X)),
         mark(g(X)) -> active(g(mark(X))),
          mark(a()) -> active(a()),
         f(mark(X)) -> f(X),
       f(active(X)) -> f(X),
         g(mark(X)) -> g(X),
       g(active(X)) -> g(X),
  active(f(f(a()))) -> mark(f(g(f(a()))))}
 DP:
  Strict:
   {       mark#(f(X)) -> active#(f(X)),
           mark#(g(X)) -> mark#(X),
           mark#(g(X)) -> g#(mark(X)),
           mark#(g(X)) -> active#(g(mark(X))),
            mark#(a()) -> active#(a()),
           f#(mark(X)) -> f#(X),
         f#(active(X)) -> f#(X),
           g#(mark(X)) -> g#(X),
         g#(active(X)) -> g#(X),
    active#(f(f(a()))) -> mark#(f(g(f(a())))),
    active#(f(f(a()))) -> f#(g(f(a()))),
    active#(f(f(a()))) -> g#(f(a()))}
  Weak:
  {       mark(f(X)) -> active(f(X)),
          mark(g(X)) -> active(g(mark(X))),
           mark(a()) -> active(a()),
          f(mark(X)) -> f(X),
        f(active(X)) -> f(X),
          g(mark(X)) -> g(X),
        g(active(X)) -> g(X),
   active(f(f(a()))) -> mark(f(g(f(a()))))}
  EDG:
   {(f#(mark(X)) -> f#(X), f#(active(X)) -> f#(X))
    (f#(mark(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (g#(mark(X)) -> g#(X), g#(active(X)) -> g#(X))
    (g#(mark(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (mark#(g(X)) -> g#(mark(X)), g#(active(X)) -> g#(X))
    (mark#(g(X)) -> g#(mark(X)), g#(mark(X)) -> g#(X))
    (active#(f(f(a()))) -> mark#(f(g(f(a())))), mark#(f(X)) -> active#(f(X)))
    (mark#(f(X)) -> active#(f(X)), active#(f(f(a()))) -> mark#(f(g(f(a())))))
    (mark#(f(X)) -> active#(f(X)), active#(f(f(a()))) -> f#(g(f(a()))))
    (mark#(f(X)) -> active#(f(X)), active#(f(f(a()))) -> g#(f(a())))
    (g#(active(X)) -> g#(X), g#(mark(X)) -> g#(X))
    (g#(active(X)) -> g#(X), g#(active(X)) -> g#(X))
    (f#(active(X)) -> f#(X), f#(mark(X)) -> f#(X))
    (f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))
    (mark#(g(X)) -> mark#(X), mark#(f(X)) -> active#(f(X)))
    (mark#(g(X)) -> mark#(X), mark#(g(X)) -> mark#(X))
    (mark#(g(X)) -> mark#(X), mark#(g(X)) -> g#(mark(X)))
    (mark#(g(X)) -> mark#(X), mark#(g(X)) -> active#(g(mark(X))))
    (mark#(g(X)) -> mark#(X), mark#(a()) -> active#(a()))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(f(a()))) -> mark#(f(g(f(a())))))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(f(a()))) -> f#(g(f(a()))))
    (mark#(g(X)) -> active#(g(mark(X))), active#(f(f(a()))) -> g#(f(a())))}
   SCCS:
    Scc:
     {  g#(mark(X)) -> g#(X),
      g#(active(X)) -> g#(X)}
    Scc:
     {  f#(mark(X)) -> f#(X),
      f#(active(X)) -> f#(X)}
    Scc:
     {mark#(g(X)) -> mark#(X)}
    Scc:
     {       mark#(f(X)) -> active#(f(X)),
      active#(f(f(a()))) -> mark#(f(g(f(a()))))}
    SCC:
     Strict:
      {  g#(mark(X)) -> g#(X),
       g#(active(X)) -> g#(X)}
     Weak:
     {       mark(f(X)) -> active(f(X)),
             mark(g(X)) -> active(g(mark(X))),
              mark(a()) -> active(a()),
             f(mark(X)) -> f(X),
           f(active(X)) -> f(X),
             g(mark(X)) -> g(X),
           g(active(X)) -> g(X),
      active(f(f(a()))) -> mark(f(g(f(a()))))}
     SPSC:
      Simple Projection:
       pi(g#) = 0
      Strict:
       {g#(active(X)) -> g#(X)}
      EDG:
       {(g#(active(X)) -> g#(X), g#(active(X)) -> g#(X))}
       SCCS:
        Scc:
         {g#(active(X)) -> g#(X)}
        SCC:
         Strict:
          {g#(active(X)) -> g#(X)}
         Weak:
         {       mark(f(X)) -> active(f(X)),
                 mark(g(X)) -> active(g(mark(X))),
                  mark(a()) -> active(a()),
                 f(mark(X)) -> f(X),
               f(active(X)) -> f(X),
                 g(mark(X)) -> g(X),
               g(active(X)) -> g(X),
          active(f(f(a()))) -> mark(f(g(f(a()))))}
         SPSC:
          Simple Projection:
           pi(g#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {  f#(mark(X)) -> f#(X),
       f#(active(X)) -> f#(X)}
     Weak:
     {       mark(f(X)) -> active(f(X)),
             mark(g(X)) -> active(g(mark(X))),
              mark(a()) -> active(a()),
             f(mark(X)) -> f(X),
           f(active(X)) -> f(X),
             g(mark(X)) -> g(X),
           g(active(X)) -> g(X),
      active(f(f(a()))) -> mark(f(g(f(a()))))}
     SPSC:
      Simple Projection:
       pi(f#) = 0
      Strict:
       {f#(active(X)) -> f#(X)}
      EDG:
       {(f#(active(X)) -> f#(X), f#(active(X)) -> f#(X))}
       SCCS:
        Scc:
         {f#(active(X)) -> f#(X)}
        SCC:
         Strict:
          {f#(active(X)) -> f#(X)}
         Weak:
         {       mark(f(X)) -> active(f(X)),
                 mark(g(X)) -> active(g(mark(X))),
                  mark(a()) -> active(a()),
                 f(mark(X)) -> f(X),
               f(active(X)) -> f(X),
                 g(mark(X)) -> g(X),
               g(active(X)) -> g(X),
          active(f(f(a()))) -> mark(f(g(f(a()))))}
         SPSC:
          Simple Projection:
           pi(f#) = 0
          Strict:
           {}
          Qed
    SCC:
     Strict:
      {mark#(g(X)) -> mark#(X)}
     Weak:
     {       mark(f(X)) -> active(f(X)),
             mark(g(X)) -> active(g(mark(X))),
              mark(a()) -> active(a()),
             f(mark(X)) -> f(X),
           f(active(X)) -> f(X),
             g(mark(X)) -> g(X),
           g(active(X)) -> g(X),
      active(f(f(a()))) -> mark(f(g(f(a()))))}
     SPSC:
      Simple Projection:
       pi(mark#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {       mark#(f(X)) -> active#(f(X)),
       active#(f(f(a()))) -> mark#(f(g(f(a()))))}
     Weak:
     {       mark(f(X)) -> active(f(X)),
             mark(g(X)) -> active(g(mark(X))),
              mark(a()) -> active(a()),
             f(mark(X)) -> f(X),
           f(active(X)) -> f(X),
             g(mark(X)) -> g(X),
           g(active(X)) -> g(X),
      active(f(f(a()))) -> mark(f(g(f(a()))))}
     POLY:
      Argument Filtering:
       pi(active#) = 0, pi(active) = [0], pi(a) = [], pi(g) = [], pi(f) = [0], pi(mark#) = 0, pi(mark) = 0
      Usable Rules:
       {}
      Interpretation:
       [g] = 0,
       [f](x0) = x0 + 1,
       [a] = 0
      Strict:
       {mark#(f(X)) -> active#(f(X))}
      Weak:
       {       mark(f(X)) -> active(f(X)),
               mark(g(X)) -> active(g(mark(X))),
                mark(a()) -> active(a()),
               f(mark(X)) -> f(X),
             f(active(X)) -> f(X),
               g(mark(X)) -> g(X),
             g(active(X)) -> g(X),
        active(f(f(a()))) -> mark(f(g(f(a()))))}
      EDG:
       {}
       SCCS:
        
        Qed