YES
Time: 0.781485
TRS:
 {  f(mark X1, X2) -> mark f(X1, X2),
   f(ok X1, ok X2) -> ok f(X1, X2),
          g mark X -> mark g X,
            g ok X -> ok g X,
  active f(X1, X2) -> f(active X1, X2),
  active f(g X, Y) -> mark f(X, f(g X, Y)),
        active g X -> g active X,
  proper f(X1, X2) -> f(proper X1, proper X2),
        proper g X -> g proper X,
        top mark X -> top proper X,
          top ok X -> top active X}
 DP:
  DP:
   {  f#(mark X1, X2) -> f#(X1, X2),
     f#(ok X1, ok X2) -> f#(X1, X2),
            g# mark X -> g# X,
              g# ok X -> g# X,
    active# f(X1, X2) -> f#(active X1, X2),
    active# f(X1, X2) -> active# X1,
    active# f(g X, Y) -> f#(X, f(g X, Y)),
          active# g X -> g# active X,
          active# g X -> active# X,
    proper# f(X1, X2) -> f#(proper X1, proper X2),
    proper# f(X1, X2) -> proper# X1,
    proper# f(X1, X2) -> proper# X2,
          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 X1, X2) -> mark f(X1, X2),
    f(ok X1, ok X2) -> ok f(X1, X2),
           g mark X -> mark g X,
             g ok X -> ok g X,
   active f(X1, X2) -> f(active X1, X2),
   active f(g X, Y) -> mark f(X, f(g X, Y)),
         active g X -> g active X,
   proper f(X1, X2) -> f(proper X1, proper X2),
         proper g X -> g proper X,
         top mark X -> top proper X,
           top ok X -> top active X}
  UR:
   {  f(mark X1, X2) -> mark f(X1, X2),
     f(ok X1, ok X2) -> ok f(X1, X2),
            g mark X -> mark g X,
              g ok X -> ok g X,
    active f(X1, X2) -> f(active X1, X2),
    active f(g X, Y) -> mark f(X, f(g X, Y)),
          active g X -> g active X,
    proper f(X1, X2) -> f(proper X1, proper X2),
          proper g X -> g proper X,
             a(x, y) -> x,
             a(x, y) -> y}
   EDG:
    {(active# f(X1, X2) -> active# X1, active# g X -> active# X)
     (active# f(X1, X2) -> active# X1, active# g X -> g# active X)
     (active# f(X1, X2) -> active# X1, active# f(g X, Y) -> f#(X, f(g X, Y)))
     (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> active# X1)
     (active# f(X1, X2) -> active# X1, active# f(X1, X2) -> f#(active X1, X2))
     (active# g X -> g# active X, g# ok X -> g# X)
     (active# g X -> g# active X, g# mark X -> g# 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)
     (active# f(g X, Y) -> f#(X, f(g X, Y)), f#(ok X1, ok X2) -> f#(X1, X2))
     (active# f(g X, Y) -> f#(X, f(g X, Y)), f#(mark X1, X2) -> f#(X1, X2))
     (g# mark X -> g# X, g# ok X -> g# X)
     (g# mark X -> g# X, g# mark X -> g# X)
     (active# g X -> active# X, active# g X -> active# X)
     (active# g X -> active# X, active# g X -> g# active X)
     (active# g X -> active# X, active# f(g X, Y) -> f#(X, f(g X, Y)))
     (active# g X -> active# X, active# f(X1, X2) -> active# X1)
     (active# g X -> active# X, active# f(X1, X2) -> f#(active X1, X2))
     (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(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# f(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (f#(mark X1, X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (proper# f(X1, X2) -> proper# X2, proper# g X -> proper# X)
     (proper# f(X1, X2) -> proper# X2, proper# g X -> g# proper X)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X2, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (f#(ok X1, ok X2) -> f#(X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (f#(ok X1, ok X2) -> f#(X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (top# ok X -> active# X, active# f(X1, X2) -> f#(active X1, X2))
     (top# ok X -> active# X, active# f(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# f(g X, Y) -> f#(X, f(g X, Y)))
     (top# ok X -> active# X, active# g X -> g# active X)
     (top# ok X -> active# X, active# g X -> active# X)
     (proper# g X -> proper# X, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# g X -> proper# X, proper# f(X1, X2) -> proper# X1)
     (proper# g X -> proper# X, proper# f(X1, X2) -> proper# X2)
     (proper# g X -> proper# X, proper# g X -> g# proper X)
     (proper# g X -> proper# X, proper# g X -> proper# X)
     (g# ok X -> g# X, g# mark X -> g# X)
     (g# ok X -> g# X, g# ok X -> g# X)
     (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(mark X1, X2) -> f#(X1, X2))
     (proper# f(X1, X2) -> f#(proper X1, proper X2), f#(ok X1, ok X2) -> f#(X1, X2))
     (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# mark X -> g# X)
     (proper# g X -> g# proper X, g# ok X -> g# X)
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> f#(proper X1, proper X2))
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X1)
     (proper# f(X1, X2) -> proper# X1, proper# f(X1, X2) -> proper# X2)
     (proper# f(X1, X2) -> proper# X1, proper# g X -> g# proper X)
     (proper# f(X1, X2) -> proper# X1, proper# g X -> proper# X)
     (active# f(X1, X2) -> f#(active X1, X2), f#(mark X1, X2) -> f#(X1, X2))
     (active# f(X1, X2) -> f#(active X1, X2), f#(ok X1, ok X2) -> f#(X1, X2))}
    STATUS:
     arrows: 0.811728
     SCCS (5):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      Scc:
       {proper# f(X1, X2) -> proper# X1,
        proper# f(X1, X2) -> proper# X2,
              proper# g X -> proper# X}
      Scc:
       {active# f(X1, X2) -> active# X1,
              active# g X -> active# X}
      Scc:
       {g# mark X -> g# X,
          g# ok X -> g# X}
      Scc:
       { f#(mark X1, X2) -> f#(X1, X2),
        f#(ok X1, ok X2) -> f#(X1, X2)}
      
      SCC (2):
       Strict:
        {top# mark X -> top# proper X,
           top# ok X -> top# active X}
       Weak:
       {  f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
                g mark X -> mark g X,
                  g ok X -> ok g X,
        active f(X1, X2) -> f(active X1, X2),
        active f(g X, Y) -> mark f(X, f(g X, Y)),
              active g X -> g active X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper g X -> g proper X,
              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:
         [f](x0, x1) = x0,
         
         [mark](x0) = 0,
         
         [g](x0) = x0,
         
         [active](x0) = 0,
         
         [proper](x0) = 0,
         
         [ok](x0) = 1,
         
         [top](x0) = 0,
         
         [top#](x0) = x0 + 1
        Strict:
         top# ok X -> top# active X
         2 + 0X >= 1 + 0X
         top# mark X -> top# proper X
         1 + 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 g X -> g proper X
         0 + 0X >= 0 + 0X
         proper f(X1, X2) -> f(proper X1, proper X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
         active g X -> g active X
         0 + 0X >= 0 + 0X
         active f(g X, Y) -> mark f(X, f(g X, Y))
         0 + 0X + 0Y >= 0 + 0X + 0Y
         active f(X1, X2) -> f(active X1, X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
         g ok X -> ok g X
         1 + 0X >= 1 + 0X
         g mark X -> mark g X
         0 + 0X >= 0 + 0X
         f(ok X1, ok X2) -> ok f(X1, X2)
         1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
         f(mark X1, X2) -> mark f(X1, X2)
         0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
       SCCS (1):
        Scc:
         {top# mark X -> top# proper X}
        
        SCC (1):
         Strict:
          {top# mark X -> top# proper X}
         Weak:
         {  f(mark X1, X2) -> mark f(X1, X2),
           f(ok X1, ok X2) -> ok f(X1, X2),
                  g mark X -> mark g X,
                    g ok X -> ok g X,
          active f(X1, X2) -> f(active X1, X2),
          active f(g X, Y) -> mark f(X, f(g X, Y)),
                active g X -> g active X,
          proper f(X1, X2) -> f(proper X1, proper X2),
                proper g X -> g proper X,
                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:
           [f](x0, x1) = x0,
           
           [mark](x0) = 1,
           
           [g](x0) = x0,
           
           [active](x0) = 0,
           
           [proper](x0) = 0,
           
           [ok](x0) = 0,
           
           [top](x0) = 0,
           
           [top#](x0) = x0 + 1
          Strict:
           top# mark X -> top# proper 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 g X -> g proper X
           0 + 0X >= 0 + 0X
           proper f(X1, X2) -> f(proper X1, proper X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           active g X -> g active X
           0 + 0X >= 0 + 0X
           active f(g X, Y) -> mark f(X, f(g X, Y))
           0 + 0X + 0Y >= 1 + 0X + 0Y
           active f(X1, X2) -> f(active X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           g ok X -> ok g X
           0 + 0X >= 0 + 0X
           g mark X -> mark g X
           1 + 0X >= 1 + 0X
           f(ok X1, ok X2) -> ok f(X1, X2)
           0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
           f(mark X1, X2) -> mark f(X1, X2)
           1 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
         Qed
     
     
     SCC (3):
      Strict:
       {proper# f(X1, X2) -> proper# X1,
        proper# f(X1, X2) -> proper# X2,
              proper# g X -> proper# X}
      Weak:
      {  f(mark X1, X2) -> mark f(X1, X2),
        f(ok X1, ok X2) -> ok f(X1, X2),
               g mark X -> mark g X,
                 g ok X -> ok g X,
       active f(X1, X2) -> f(active X1, X2),
       active f(g X, Y) -> mark f(X, f(g X, Y)),
             active g X -> g active X,
       proper f(X1, X2) -> f(proper X1, proper X2),
             proper g X -> g proper X,
             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:
        [f](x0, x1) = x0 + x1,
        
        [mark](x0) = 0,
        
        [g](x0) = x0 + 1,
        
        [active](x0) = 0,
        
        [proper](x0) = 0,
        
        [ok](x0) = x0 + 1,
        
        [top](x0) = 0,
        
        [proper#](x0) = x0
       Strict:
        proper# g X -> proper# X
        1 + 1X >= 0 + 1X
        proper# f(X1, X2) -> proper# X2
        0 + 1X1 + 1X2 >= 0 + 1X2
        proper# f(X1, X2) -> proper# X1
        0 + 1X1 + 1X2 >= 0 + 1X1
       Weak:
        top ok X -> top active X
        0 + 0X >= 0 + 0X
        top mark X -> top proper X
        0 + 0X >= 0 + 0X
        proper g X -> g proper X
        0 + 0X >= 1 + 0X
        proper f(X1, X2) -> f(proper X1, proper X2)
        0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
        active g X -> g active X
        0 + 0X >= 1 + 0X
        active f(g X, Y) -> mark f(X, f(g X, Y))
        0 + 0X + 0Y >= 0 + 0X + 0Y
        active f(X1, X2) -> f(active X1, X2)
        0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
        g ok X -> ok g X
        2 + 1X >= 2 + 1X
        g mark X -> mark g X
        1 + 0X >= 0 + 0X
        f(ok X1, ok X2) -> ok f(X1, X2)
        2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
        f(mark X1, X2) -> mark f(X1, X2)
        0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
      SCCS (1):
       Scc:
        {proper# f(X1, X2) -> proper# X1,
         proper# f(X1, X2) -> proper# X2}
       
       SCC (2):
        Strict:
         {proper# f(X1, X2) -> proper# X1,
          proper# f(X1, X2) -> proper# X2}
        Weak:
        {  f(mark X1, X2) -> mark f(X1, X2),
          f(ok X1, ok X2) -> ok f(X1, X2),
                 g mark X -> mark g X,
                   g ok X -> ok g X,
         active f(X1, X2) -> f(active X1, X2),
         active f(g X, Y) -> mark f(X, f(g X, Y)),
               active g X -> g active X,
         proper f(X1, X2) -> f(proper X1, proper X2),
               proper g X -> g proper X,
               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:
          [f](x0, x1) = x0 + x1 + 1,
          
          [mark](x0) = x0 + 1,
          
          [g](x0) = 0,
          
          [active](x0) = x0 + 1,
          
          [proper](x0) = 0,
          
          [ok](x0) = 0,
          
          [top](x0) = 0,
          
          [proper#](x0) = x0
         Strict:
          proper# f(X1, X2) -> proper# X2
          1 + 1X1 + 1X2 >= 0 + 1X2
          proper# f(X1, X2) -> proper# X1
          1 + 1X1 + 1X2 >= 0 + 1X1
         Weak:
          top ok X -> top active X
          0 + 0X >= 0 + 0X
          top mark X -> top proper X
          0 + 0X >= 0 + 0X
          proper g X -> g proper X
          0 + 0X >= 0 + 0X
          proper f(X1, X2) -> f(proper X1, proper X2)
          0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
          active g X -> g active X
          1 + 0X >= 0 + 0X
          active f(g X, Y) -> mark f(X, f(g X, Y))
          2 + 0X + 1Y >= 3 + 1X + 1Y
          active f(X1, X2) -> f(active X1, X2)
          2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
          g ok X -> ok g X
          0 + 0X >= 0 + 0X
          g mark X -> mark g X
          0 + 0X >= 1 + 0X
          f(ok X1, ok X2) -> ok f(X1, X2)
          1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
          f(mark X1, X2) -> mark f(X1, X2)
          2 + 1X1 + 1X2 >= 2 + 1X1 + 1X2
        Qed
    
    
    SCC (2):
     Strict:
      {active# f(X1, X2) -> active# X1,
             active# g X -> active# X}
     Weak:
     {  f(mark X1, X2) -> mark f(X1, X2),
       f(ok X1, ok X2) -> ok f(X1, X2),
              g mark X -> mark g X,
                g ok X -> ok g X,
      active f(X1, X2) -> f(active X1, X2),
      active f(g X, Y) -> mark f(X, f(g X, Y)),
            active g X -> g active X,
      proper f(X1, X2) -> f(proper X1, proper X2),
            proper g X -> g proper X,
            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:
       [f](x0, x1) = x0 + x1,
       
       [mark](x0) = 0,
       
       [g](x0) = x0 + 1,
       
       [active](x0) = 0,
       
       [proper](x0) = 0,
       
       [ok](x0) = x0 + 1,
       
       [top](x0) = 0,
       
       [active#](x0) = x0
      Strict:
       active# g X -> active# X
       1 + 1X >= 0 + 1X
       active# f(X1, X2) -> active# X1
       0 + 1X1 + 1X2 >= 0 + 1X1
      Weak:
       top ok X -> top active X
       0 + 0X >= 0 + 0X
       top mark X -> top proper X
       0 + 0X >= 0 + 0X
       proper g X -> g proper X
       0 + 0X >= 1 + 0X
       proper f(X1, X2) -> f(proper X1, proper X2)
       0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
       active g X -> g active X
       0 + 0X >= 1 + 0X
       active f(g X, Y) -> mark f(X, f(g X, Y))
       0 + 0X + 0Y >= 0 + 0X + 0Y
       active f(X1, X2) -> f(active X1, X2)
       0 + 0X1 + 0X2 >= 0 + 0X1 + 1X2
       g ok X -> ok g X
       2 + 1X >= 2 + 1X
       g mark X -> mark g X
       1 + 0X >= 0 + 0X
       f(ok X1, ok X2) -> ok f(X1, X2)
       2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
       f(mark X1, X2) -> mark f(X1, X2)
       0 + 0X1 + 1X2 >= 0 + 0X1 + 0X2
     SCCS (1):
      Scc:
       {active# f(X1, X2) -> active# X1}
      
      SCC (1):
       Strict:
        {active# f(X1, X2) -> active# X1}
       Weak:
       {  f(mark X1, X2) -> mark f(X1, X2),
         f(ok X1, ok X2) -> ok f(X1, X2),
                g mark X -> mark g X,
                  g ok X -> ok g X,
        active f(X1, X2) -> f(active X1, X2),
        active f(g X, Y) -> mark f(X, f(g X, Y)),
              active g X -> g active X,
        proper f(X1, X2) -> f(proper X1, proper X2),
              proper g X -> g proper X,
              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:
         [f](x0, x1) = x0 + 1,
         
         [mark](x0) = x0 + 1,
         
         [g](x0) = x0 + 1,
         
         [active](x0) = x0 + 1,
         
         [proper](x0) = 0,
         
         [ok](x0) = x0 + 1,
         
         [top](x0) = 0,
         
         [active#](x0) = x0
        Strict:
         active# f(X1, X2) -> active# X1
         1 + 1X1 + 0X2 >= 0 + 1X1
        Weak:
         top ok X -> top active X
         0 + 0X >= 0 + 0X
         top mark X -> top proper X
         0 + 0X >= 0 + 0X
         proper g X -> g proper X
         0 + 0X >= 1 + 0X
         proper f(X1, X2) -> f(proper X1, proper X2)
         0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
         active g X -> g active X
         2 + 1X >= 2 + 1X
         active f(g X, Y) -> mark f(X, f(g X, Y))
         3 + 1X + 0Y >= 2 + 1X + 0Y
         active f(X1, X2) -> f(active X1, X2)
         2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
         g ok X -> ok g X
         2 + 1X >= 2 + 1X
         g mark X -> mark g X
         2 + 1X >= 2 + 1X
         f(ok X1, ok X2) -> ok f(X1, X2)
         2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
         f(mark X1, X2) -> mark f(X1, X2)
         2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
       Qed
   
   SCC (2):
    Strict:
     {g# mark X -> g# X,
        g# ok X -> g# X}
    Weak:
    {  f(mark X1, X2) -> mark f(X1, X2),
      f(ok X1, ok X2) -> ok f(X1, X2),
             g mark X -> mark g X,
               g ok X -> ok g X,
     active f(X1, X2) -> f(active X1, X2),
     active f(g X, Y) -> mark f(X, f(g X, Y)),
           active g X -> g active X,
     proper f(X1, X2) -> f(proper X1, proper X2),
           proper g X -> g proper X,
           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:
      [f](x0, x1) = 0,
      
      [mark](x0) = x0,
      
      [g](x0) = 0,
      
      [active](x0) = 0,
      
      [proper](x0) = 0,
      
      [ok](x0) = x0 + 1,
      
      [top](x0) = 0,
      
      [g#](x0) = x0
     Strict:
      g# ok X -> g# X
      1 + 1X >= 0 + 1X
      g# mark X -> g# 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 g X -> g proper X
      0 + 0X >= 0 + 0X
      proper f(X1, X2) -> f(proper X1, proper X2)
      0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
      active g X -> g active X
      0 + 0X >= 0 + 0X
      active f(g X, Y) -> mark f(X, f(g X, Y))
      0 + 0X + 0Y >= 0 + 0X + 0Y
      active f(X1, X2) -> f(active X1, X2)
      0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
      g ok X -> ok g X
      0 + 0X >= 1 + 0X
      g mark X -> mark g X
      0 + 0X >= 0 + 0X
      f(ok X1, ok X2) -> ok f(X1, X2)
      0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
      f(mark X1, X2) -> mark f(X1, X2)
      0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2
    SCCS (1):
     Scc:
      {g# mark X -> g# X}
     
     SCC (1):
      Strict:
       {g# mark X -> g# X}
      Weak:
      {  f(mark X1, X2) -> mark f(X1, X2),
        f(ok X1, ok X2) -> ok f(X1, X2),
               g mark X -> mark g X,
                 g ok X -> ok g X,
       active f(X1, X2) -> f(active X1, X2),
       active f(g X, Y) -> mark f(X, f(g X, Y)),
             active g X -> g active X,
       proper f(X1, X2) -> f(proper X1, proper X2),
             proper g X -> g proper X,
             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:
        [f](x0, x1) = x0 + 1,
        
        [mark](x0) = x0 + 1,
        
        [g](x0) = x0 + 1,
        
        [active](x0) = x0 + 1,
        
        [proper](x0) = 0,
        
        [ok](x0) = x0 + 1,
        
        [top](x0) = 0,
        
        [g#](x0) = x0
       Strict:
        g# mark X -> g# 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 g X -> g proper X
        0 + 0X >= 1 + 0X
        proper f(X1, X2) -> f(proper X1, proper X2)
        0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
        active g X -> g active X
        2 + 1X >= 2 + 1X
        active f(g X, Y) -> mark f(X, f(g X, Y))
        3 + 1X + 0Y >= 2 + 1X + 0Y
        active f(X1, X2) -> f(active X1, X2)
        2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
        g ok X -> ok g X
        2 + 1X >= 2 + 1X
        g mark X -> mark g X
        2 + 1X >= 2 + 1X
        f(ok X1, ok X2) -> ok f(X1, X2)
        2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
        f(mark X1, X2) -> mark f(X1, X2)
        2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
      Qed
  
  
  SCC (2):
   Strict:
    { f#(mark X1, X2) -> f#(X1, X2),
     f#(ok X1, ok X2) -> f#(X1, X2)}
   Weak:
   {  f(mark X1, X2) -> mark f(X1, X2),
     f(ok X1, ok X2) -> ok f(X1, X2),
            g mark X -> mark g X,
              g ok X -> ok g X,
    active f(X1, X2) -> f(active X1, X2),
    active f(g X, Y) -> mark f(X, f(g X, Y)),
          active g X -> g active X,
    proper f(X1, X2) -> f(proper X1, proper X2),
          proper g X -> g proper X,
          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:
     [f](x0, x1) = x0 + 1,
     
     [mark](x0) = x0 + 1,
     
     [g](x0) = x0 + 1,
     
     [active](x0) = x0 + 1,
     
     [proper](x0) = x0 + 1,
     
     [ok](x0) = x0 + 1,
     
     [top](x0) = 0,
     
     [f#](x0, x1) = x0
    Strict:
     f#(ok X1, ok X2) -> f#(X1, X2)
     1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
     f#(mark X1, X2) -> f#(X1, X2)
     0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2
    Weak:
     top ok X -> top active X
     0 + 0X >= 0 + 0X
     top mark X -> top proper X
     0 + 0X >= 0 + 0X
     proper g X -> g proper X
     2 + 1X >= 2 + 1X
     proper f(X1, X2) -> f(proper X1, proper X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     active g X -> g active X
     2 + 1X >= 2 + 1X
     active f(g X, Y) -> mark f(X, f(g X, Y))
     3 + 1X + 0Y >= 2 + 1X + 0Y
     active f(X1, X2) -> f(active X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     g ok X -> ok g X
     2 + 1X >= 2 + 1X
     g mark X -> mark g X
     2 + 1X >= 2 + 1X
     f(ok X1, ok X2) -> ok f(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     f(mark X1, X2) -> mark f(X1, X2)
     2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
   SCCS (1):
    Scc:
     {f#(mark X1, X2) -> f#(X1, X2)}
    
    SCC (1):
     Strict:
      {f#(mark X1, X2) -> f#(X1, X2)}
     Weak:
     {  f(mark X1, X2) -> mark f(X1, X2),
       f(ok X1, ok X2) -> ok f(X1, X2),
              g mark X -> mark g X,
                g ok X -> ok g X,
      active f(X1, X2) -> f(active X1, X2),
      active f(g X, Y) -> mark f(X, f(g X, Y)),
            active g X -> g active X,
      proper f(X1, X2) -> f(proper X1, proper X2),
            proper g X -> g proper X,
            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:
       [f](x0, x1) = x0 + 1,
       
       [mark](x0) = x0 + 1,
       
       [g](x0) = x0 + 1,
       
       [active](x0) = x0 + 1,
       
       [proper](x0) = 0,
       
       [ok](x0) = x0 + 1,
       
       [top](x0) = 0,
       
       [f#](x0, x1) = x0
      Strict:
       f#(mark X1, X2) -> f#(X1, X2)
       1 + 1X1 + 0X2 >= 0 + 1X1 + 0X2
      Weak:
       top ok X -> top active X
       0 + 0X >= 0 + 0X
       top mark X -> top proper X
       0 + 0X >= 0 + 0X
       proper g X -> g proper X
       0 + 0X >= 1 + 0X
       proper f(X1, X2) -> f(proper X1, proper X2)
       0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2
       active g X -> g active X
       2 + 1X >= 2 + 1X
       active f(g X, Y) -> mark f(X, f(g X, Y))
       3 + 1X + 0Y >= 2 + 1X + 0Y
       active f(X1, X2) -> f(active X1, X2)
       2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
       g ok X -> ok g X
       2 + 1X >= 2 + 1X
       g mark X -> mark g X
       2 + 1X >= 2 + 1X
       f(ok X1, ok X2) -> ok f(X1, X2)
       2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
       f(mark X1, X2) -> mark f(X1, X2)
       2 + 1X1 + 0X2 >= 2 + 1X1 + 0X2
     Qed