YES(?,O(n^2))
TRS:
 {
    f mark X -> mark f X,
      f ok X -> ok f X,
      g ok X -> ok g X,
    h mark X -> mark h X,
      h ok X -> ok h X,
  active f X -> f active X,
  active f X -> mark g h f X,
  active h X -> h active X,
  proper f X -> f proper X,
  proper g X -> g proper X,
  proper h X -> h proper X,
  top mark X -> top proper X,
    top ok X -> top active X
 }
 DUP: We consider a non-duplicating system.
  Trs:
   {
      f mark X -> mark f X,
        f ok X -> ok f X,
        g ok X -> ok g X,
      h mark X -> mark h X,
        h ok X -> ok h X,
    active f X -> f active X,
    active f X -> mark g h f X,
    active h X -> h active X,
    proper f X -> f proper X,
    proper g X -> g proper X,
    proper h X -> h proper X,
    top mark X -> top proper X,
      top ok X -> top active X
   }
  Matrix Interpretation:
   Interpretation class: triangular
         [X1]    [1 5][X1]   [0]
   [top]([X0]) = [0 0][X0] + [0]
   
        [X1]    [1 6][X1]   [0]
   [ok]([X0]) = [0 1][X0] + [7]
   
            [X1]    [1 1][X1]   [0]
   [proper]([X0]) = [0 1][X0] + [0]
   
            [X1]    [1 6][X1]   [4]
   [active]([X0]) = [0 1][X0] + [5]
   
          [X1]    [1 1][X1]   [4]
   [mark]([X0]) = [0 1][X0] + [2]
   
       [X1]    [1 2][X1]   [0]
   [h]([X0]) = [0 1][X0] + [2]
   
       [X1]    [1 1][X1]   [0]
   [g]([X0]) = [0 1][X0] + [1]
   
       [X1]    [1 4][X1]   [7]
   [f]([X0]) = [0 1][X0] + [4]
   
   
   Qed