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