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