YES
Time: 0.081346
TRS:
 {      f mark X -> mark f X,
          f ok X -> ok f X,
          g ok X -> ok g X,
      active f X -> f active X,
  active f f a() -> mark f g f a(),
      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:
   {      f# mark X -> f# X,
            f# ok X -> f# X,
            g# ok X -> g# X,
        active# f X -> f# active X,
        active# f X -> active# X,
    active# f f a() -> f# g f a(),
    active# f f a() -> g# f a(),
        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:
  {      f mark X -> mark f X,
           f ok X -> ok f X,
           g ok X -> ok g X,
       active f X -> f active X,
   active f f a() -> mark f g f a(),
       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:
   {      f mark X -> mark f X,
            f ok X -> ok f X,
            g ok X -> ok g X,
        active f X -> f active X,
    active f f a() -> mark f g f a(),
        proper f X -> f proper X,
        proper g X -> g proper X,
        proper a() -> ok a()}
   EDG:
    {(proper# f X -> f# proper X, f# ok X -> f# X)
     (proper# f X -> f# proper X, f# mark X -> f# 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)
     (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)
     (proper# f X -> proper# X, proper# g X -> proper# X)
     (proper# f X -> proper# X, proper# g X -> g# proper X)
     (proper# f X -> proper# X, proper# f X -> proper# X)
     (proper# f X -> proper# X, proper# f X -> f# proper X)
     (top# mark X -> proper# X, proper# g X -> proper# X)
     (top# mark 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# ok X -> active# X, active# f X -> f# active X)
     (top# ok X -> active# X, active# f X -> active# X)
     (top# ok X -> active# X, active# f f a() -> f# g f a())
     (top# ok X -> active# X, active# f f a() -> g# f a())
     (proper# g X -> proper# X, proper# f X -> f# proper X)
     (proper# g 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)
     (active# f X -> active# X, active# f X -> f# active X)
     (active# f X -> active# X, active# f X -> active# X)
     (active# f X -> active# X, active# f f a() -> f# g f a())
     (active# f X -> active# X, active# f f a() -> g# f a())
     (f# ok X -> f# X, f# mark X -> f# X)
     (f# ok X -> f# X, f# ok X -> f# 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# g X -> g# proper X, g# ok X -> g# X)
     (active# f X -> f# active X, f# mark X -> f# X)
     (active# f X -> f# active X, f# ok X -> f# X)}
    STATUS:
     arrows: 0.831111
     SCCS (5):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {active# f X -> active# X}
      Scc:
       {proper# f X -> proper# X,
        proper# g X -> proper# X}
      Scc:
       {g# ok X -> g# X}
      Scc:
       {f# mark X -> f# X,
          f# ok X -> f# X}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {      f mark X -> mark f X,
                f ok X -> ok f X,
                g ok X -> ok g X,
            active f X -> f active X,
        active f f a() -> mark f g f a(),
            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,
         
         [f](x0) = x0,
         
         [g](x0) = 0,
         
         [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 + 0X >= 0 + 0X
         proper f X -> f proper X
         0 + 1X >= 0 + 1X
         active f f a() -> mark f g f a()
         1 >= 1
         active f X -> f active X
         0 + 1X >= 0 + 1X
         g ok X -> ok g X
         0 + 0X >= 0 + 0X
         f ok X -> ok f X
         0 + 1X >= 0 + 1X
         f mark X -> mark f X
         1 + 1X >= 1 + 1X
       SCCS (1):
        Scc:
         {top# ok X -> top# active X}
        
        SCC (1):
         Strict:
          {top# ok X -> top# active X}
         Weak:
         {      f mark X -> mark f X,
                  f ok X -> ok f X,
                  g ok X -> ok g X,
              active f X -> f active X,
          active f f a() -> mark f g f a(),
              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,
           
           [f](x0) = x0,
           
           [g](x0) = x0 + 1,
           
           [active](x0) = 0,
           
           [proper](x0) = 0,
           
           [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()
           0 >= 1
           proper g X -> g proper X
           0 + 0X >= 1 + 0X
           proper f X -> f proper X
           0 + 0X >= 0 + 0X
           active f f a() -> mark f g f a()
           0 >= 0
           active f X -> f active X
           0 + 0X >= 0 + 0X
           g ok X -> ok g X
           2 + 0X >= 1 + 0X
           f ok X -> ok f X
           1 + 0X >= 1 + 0X
           f mark X -> mark f X
           0 + 0X >= 0 + 0X
         Qed
     
     SCC (1):
      Strict:
       {active# f X -> active# X}
      Weak:
      {      f mark X -> mark f X,
               f ok X -> ok f X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark f g f a(),
           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,
        
        [f](x0) = x0 + 1,
        
        [g](x0) = 0,
        
        [active](x0) = x0 + 1,
        
        [proper](x0) = x0 + 1,
        
        [ok](x0) = x0 + 1,
        
        [top](x0) = x0,
        
        [a] = 1,
        
        [active#](x0) = x0 + 1
       Strict:
        active# f X -> active# X
        2 + 1X >= 1 + 1X
       Weak:
        top ok X -> top active X
        1 + 1X >= 1 + 1X
        top mark X -> top proper X
        0 + 0X >= 1 + 1X
        proper a() -> ok a()
        2 >= 2
        proper g X -> g proper X
        1 + 0X >= 0 + 0X
        proper f X -> f proper X
        2 + 1X >= 2 + 1X
        active f f a() -> mark f g f a()
        4 >= 0
        active f X -> f active X
        2 + 1X >= 2 + 1X
        g ok X -> ok g X
        0 + 0X >= 1 + 0X
        f ok X -> ok f X
        2 + 1X >= 2 + 1X
        f mark X -> mark f X
        1 + 0X >= 0 + 0X
      Qed
    
    SCC (2):
     Strict:
      {proper# f X -> proper# X,
       proper# g X -> proper# X}
     Weak:
     {      f mark X -> mark f X,
              f ok X -> ok f X,
              g ok X -> ok g X,
          active f X -> f active X,
      active f f a() -> mark f g f a(),
          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,
       
       [f](x0) = x0,
       
       [g](x0) = x0 + 1,
       
       [active](x0) = 0,
       
       [proper](x0) = 0,
       
       [ok](x0) = 0,
       
       [top](x0) = 0,
       
       [a] = 1,
       
       [proper#](x0) = x0
      Strict:
       proper# g X -> proper# X
       1 + 1X >= 0 + 1X
       proper# f X -> proper# X
       0 + 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()
       0 >= 0
       proper g X -> g proper X
       0 + 0X >= 1 + 0X
       proper f X -> f proper X
       0 + 0X >= 0 + 0X
       active f f a() -> mark f g f a()
       0 >= 2
       active f X -> f active X
       0 + 0X >= 0 + 0X
       g ok X -> ok g X
       1 + 0X >= 0 + 0X
       f ok X -> ok f X
       0 + 0X >= 0 + 0X
       f mark X -> mark f X
       0 + 1X >= 0 + 1X
     SCCS (1):
      Scc:
       {proper# f X -> proper# X}
      
      SCC (1):
       Strict:
        {proper# f X -> proper# X}
       Weak:
       {      f mark X -> mark f X,
                f ok X -> ok f X,
                g ok X -> ok g X,
            active f X -> f active X,
        active f f a() -> mark f g f a(),
            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,
         
         [f](x0) = x0 + 1,
         
         [g](x0) = 0,
         
         [active](x0) = x0 + 1,
         
         [proper](x0) = x0 + 1,
         
         [ok](x0) = x0 + 1,
         
         [top](x0) = x0,
         
         [a] = 1,
         
         [proper#](x0) = x0 + 1
        Strict:
         proper# f X -> proper# X
         2 + 1X >= 1 + 1X
        Weak:
         top ok X -> top active X
         1 + 1X >= 1 + 1X
         top mark X -> top proper X
         0 + 0X >= 1 + 1X
         proper a() -> ok a()
         2 >= 2
         proper g X -> g proper X
         1 + 0X >= 0 + 0X
         proper f X -> f proper X
         2 + 1X >= 2 + 1X
         active f f a() -> mark f g f a()
         4 >= 0
         active f X -> f active X
         2 + 1X >= 2 + 1X
         g ok X -> ok g X
         0 + 0X >= 1 + 0X
         f ok X -> ok f X
         2 + 1X >= 2 + 1X
         f mark X -> mark f X
         1 + 0X >= 0 + 0X
       Qed
   
   SCC (1):
    Strict:
     {g# ok X -> g# X}
    Weak:
    {      f mark X -> mark f X,
             f ok X -> ok f X,
             g ok X -> ok g X,
         active f X -> f active X,
     active f f a() -> mark f g f a(),
         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,
      
      [f](x0) = x0 + 1,
      
      [g](x0) = 0,
      
      [active](x0) = x0 + 1,
      
      [proper](x0) = x0 + 1,
      
      [ok](x0) = x0 + 1,
      
      [top](x0) = 0,
      
      [a] = 1,
      
      [g#](x0) = x0 + 1
     Strict:
      g# ok X -> g# X
      2 + 1X >= 1 + 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()
      2 >= 2
      proper g X -> g proper X
      1 + 0X >= 0 + 0X
      proper f X -> f proper X
      2 + 1X >= 2 + 1X
      active f f a() -> mark f g f a()
      4 >= 2
      active f X -> f active X
      2 + 1X >= 2 + 1X
      g ok X -> ok g X
      0 + 0X >= 1 + 0X
      f ok X -> ok f X
      2 + 1X >= 2 + 1X
      f mark X -> mark f X
      2 + 1X >= 2 + 1X
    Qed
   
   
   SCC (2):
    Strict:
     {f# mark X -> f# X,
        f# ok X -> f# X}
    Weak:
    {      f mark X -> mark f X,
             f ok X -> ok f X,
             g ok X -> ok g X,
         active f X -> f active X,
     active f f a() -> mark f g f a(),
         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,
      
      [f](x0) = 0,
      
      [g](x0) = x0 + 1,
      
      [active](x0) = 0,
      
      [proper](x0) = 0,
      
      [ok](x0) = x0 + 1,
      
      [top](x0) = 0,
      
      [a] = 1,
      
      [f#](x0) = x0
     Strict:
      f# ok X -> f# X
      1 + 1X >= 0 + 1X
      f# mark X -> f# X
      0 + 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()
      0 >= 2
      proper g X -> g proper X
      0 + 0X >= 1 + 0X
      proper f X -> f proper X
      0 + 0X >= 0 + 0X
      active f f a() -> mark f g f a()
      0 >= 0
      active f X -> f active X
      0 + 0X >= 0 + 0X
      g ok X -> ok g X
      2 + 1X >= 2 + 1X
      f ok X -> ok f X
      0 + 0X >= 1 + 0X
      f mark X -> mark f X
      0 + 0X >= 0 + 0X
    SCCS (1):
     Scc:
      {f# mark X -> f# X}
     
     SCC (1):
      Strict:
       {f# mark X -> f# X}
      Weak:
      {      f mark X -> mark f X,
               f ok X -> ok f X,
               g ok X -> ok g X,
           active f X -> f active X,
       active f f a() -> mark f g f a(),
           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,
        
        [f](x0) = x0 + 1,
        
        [g](x0) = 0,
        
        [active](x0) = x0 + 1,
        
        [proper](x0) = x0 + 1,
        
        [ok](x0) = x0 + 1,
        
        [top](x0) = 0,
        
        [a] = 1,
        
        [f#](x0) = x0
       Strict:
        f# mark X -> f# 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()
        2 >= 2
        proper g X -> g proper X
        1 + 0X >= 0 + 0X
        proper f X -> f proper X
        2 + 1X >= 2 + 1X
        active f f a() -> mark f g f a()
        4 >= 2
        active f X -> f active X
        2 + 1X >= 2 + 1X
        g ok X -> ok g X
        0 + 0X >= 1 + 0X
        f ok X -> ok f X
        2 + 1X >= 2 + 1X
        f mark X -> mark f X
        2 + 1X >= 2 + 1X
      Qed