YES
Time: 0.048782
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:
  DP:
   {        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}
  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}
  UR:
   {        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()}
   EDG:
    {(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)
     (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# ok X -> f# X)
     (active# g X -> g# active X, g# mark X -> g# X)}
    STATUS:
     arrows: 0.973140
     SCCS (1):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      
      SCC (2):
       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:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [mark](x0) = x0 + 1,
         
         [c](x0) = 0,
         
         [f](x0) = x0,
         
         [g](x0) = x0,
         
         [active](x0) = x0,
         
         [proper](x0) = x0,
         
         [ok](x0) = x0,
         
         [top](x0) = 0,
         
         [a] = 1,
         
         [top#](x0) = x0
        Strict:
         top# ok X -> top# active X
         0 + 1X >= 0 + 1X
         top# mark X -> top# proper X
         1 + 1X >= 0 + 1X
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper a() -> ok a()
         1 >= 1
         proper g X -> g proper X
         0 + 1X >= 0 + 1X
         proper f X -> f proper X
         0 + 1X >= 0 + 1X
         proper c X -> c proper X
         0 + 0X >= 0 + 0X
         active g X -> g active X
         0 + 1X >= 0 + 1X
         active f f a() -> mark c f g f a()
         1 >= 1
         active f X -> f active X
         0 + 1X >= 0 + 1X
         g ok X -> ok g X
         0 + 1X >= 0 + 1X
         g mark X -> mark g X
         1 + 1X >= 1 + 1X
         f ok X -> ok f X
         0 + 1X >= 0 + 1X
         f mark X -> mark f X
         1 + 1X >= 1 + 1X
         c ok X -> ok c X
         0 + 0X >= 0 + 0X
       SCCS (1):
        Scc:
         {top# ok X -> top# active X}
        
        SCC (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}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [mark](x0) = 0,
           
           [c](x0) = x0 + 1,
           
           [f](x0) = x0,
           
           [g](x0) = x0,
           
           [active](x0) = 0,
           
           [proper](x0) = x0 + 1,
           
           [ok](x0) = 1,
           
           [top](x0) = 0,
           
           [a] = 0,
           
           [top#](x0) = x0 + 1
          Strict:
           top# ok X -> top# active X
           2 + 0X >= 1 + 0X
          Weak:
           top ok X -> top active X
           0 + 0X >= 0 + 0X
           top mark X -> top proper X
           0 + 0X >= 0 + 0X
           proper a() -> ok a()
           1 >= 1
           proper g X -> g proper X
           1 + 1X >= 1 + 1X
           proper f X -> f proper X
           1 + 1X >= 1 + 1X
           proper c X -> c proper X
           2 + 1X >= 2 + 1X
           active g X -> g active X
           0 + 0X >= 0 + 0X
           active f f a() -> mark c f g f a()
           0 >= 0
           active f X -> f active X
           0 + 0X >= 0 + 0X
           g ok X -> ok g X
           1 + 0X >= 1 + 0X
           g mark X -> mark g X
           0 + 0X >= 0 + 0X
           f ok X -> ok f X
           1 + 0X >= 1 + 0X
           f mark X -> mark f X
           0 + 0X >= 0 + 0X
           c ok X -> ok c X
           2 + 0X >= 1 + 0X
         Qed