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