We consider the following Problem:

  Strict Trs:
    {  active(f(x)) -> mark(x)
     , top(active(c())) -> top(mark(c()))
     , top(mark(x)) -> top(check(x))
     , check(f(x)) -> f(check(x))
     , check(x) -> start(match(f(X()), x))
     , match(f(x), f(y)) -> f(match(x, y))
     , match(X(), x) -> proper(x)
     , proper(c()) -> ok(c())
     , proper(f(x)) -> f(proper(x))
     , f(ok(x)) -> ok(f(x))
     , start(ok(x)) -> found(x)
     , f(found(x)) -> found(f(x))
     , top(found(x)) -> top(active(x))
     , active(f(x)) -> f(active(x))
     , f(mark(x)) -> mark(f(x))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^1))

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  active(f(x)) -> mark(x)
       , top(active(c())) -> top(mark(c()))
       , top(mark(x)) -> top(check(x))
       , check(f(x)) -> f(check(x))
       , check(x) -> start(match(f(X()), x))
       , match(f(x), f(y)) -> f(match(x, y))
       , match(X(), x) -> proper(x)
       , proper(c()) -> ok(c())
       , proper(f(x)) -> f(proper(x))
       , f(ok(x)) -> ok(f(x))
       , start(ok(x)) -> found(x)
       , f(found(x)) -> found(f(x))
       , top(found(x)) -> top(active(x))
       , active(f(x)) -> f(active(x))
       , f(mark(x)) -> mark(f(x))}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    The weightgap principle applies, where following rules are oriented strictly:
    
    TRS Component:
      {  active(f(x)) -> mark(x)
       , top(active(c())) -> top(mark(c()))
       , start(ok(x)) -> found(x)}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
        Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
        Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
        Uargs(found) = {1}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       active(x1) = [1 0] x1 + [1]
                    [1 0]      [1]
       f(x1) = [1 0] x1 + [0]
               [0 0]      [1]
       mark(x1) = [1 0] x1 + [0]
                  [0 0]      [1]
       top(x1) = [1 0] x1 + [0]
                 [0 0]      [1]
       c() = [0]
             [0]
       check(x1) = [0 0] x1 + [0]
                   [0 0]      [1]
       start(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
       match(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                       [0 0]      [0 0]      [1]
       X() = [0]
             [0]
       proper(x1) = [0 0] x1 + [1]
                    [0 0]      [1]
       ok(x1) = [1 0] x1 + [1]
                [0 0]      [1]
       found(x1) = [1 0] x1 + [0]
                   [0 0]      [1]
    
    The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  top(mark(x)) -> top(check(x))
         , check(f(x)) -> f(check(x))
         , check(x) -> start(match(f(X()), x))
         , match(f(x), f(y)) -> f(match(x, y))
         , match(X(), x) -> proper(x)
         , proper(c()) -> ok(c())
         , proper(f(x)) -> f(proper(x))
         , f(ok(x)) -> ok(f(x))
         , f(found(x)) -> found(f(x))
         , top(found(x)) -> top(active(x))
         , active(f(x)) -> f(active(x))
         , f(mark(x)) -> mark(f(x))}
      Weak Trs:
        {  active(f(x)) -> mark(x)
         , top(active(c())) -> top(mark(c()))
         , start(ok(x)) -> found(x)}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {proper(c()) -> ok(c())}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
          Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
          Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
          Uargs(found) = {1}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         active(x1) = [1 0] x1 + [0]
                      [0 0]      [1]
         f(x1) = [1 0] x1 + [1]
                 [0 0]      [1]
         mark(x1) = [1 0] x1 + [0]
                    [0 0]      [1]
         top(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
         c() = [0]
               [0]
         check(x1) = [0 0] x1 + [0]
                     [0 0]      [1]
         start(x1) = [1 0] x1 + [1]
                     [0 0]      [1]
         match(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                         [0 0]      [0 0]      [1]
         X() = [0]
               [0]
         proper(x1) = [0 0] x1 + [1]
                      [0 0]      [1]
         ok(x1) = [1 0] x1 + [0]
                  [0 0]      [1]
         found(x1) = [1 0] x1 + [0]
                     [0 0]      [1]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs:
          {  top(mark(x)) -> top(check(x))
           , check(f(x)) -> f(check(x))
           , check(x) -> start(match(f(X()), x))
           , match(f(x), f(y)) -> f(match(x, y))
           , match(X(), x) -> proper(x)
           , proper(f(x)) -> f(proper(x))
           , f(ok(x)) -> ok(f(x))
           , f(found(x)) -> found(f(x))
           , top(found(x)) -> top(active(x))
           , active(f(x)) -> f(active(x))
           , f(mark(x)) -> mark(f(x))}
        Weak Trs:
          {  proper(c()) -> ok(c())
           , active(f(x)) -> mark(x)
           , top(active(c())) -> top(mark(c()))
           , start(ok(x)) -> found(x)}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component: {top(found(x)) -> top(active(x))}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
            Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
            Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
            Uargs(found) = {1}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           active(x1) = [1 0] x1 + [0]
                        [0 0]      [1]
           f(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
           mark(x1) = [1 0] x1 + [0]
                      [0 0]      [1]
           top(x1) = [1 0] x1 + [1]
                     [0 0]      [1]
           c() = [0]
                 [0]
           check(x1) = [0 0] x1 + [0]
                       [0 0]      [1]
           start(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
           match(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                           [0 0]      [0 0]      [1]
           X() = [0]
                 [0]
           proper(x1) = [0 0] x1 + [1]
                        [0 0]      [1]
           ok(x1) = [1 0] x1 + [0]
                    [0 0]      [1]
           found(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
        
        The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Strict Trs:
            {  top(mark(x)) -> top(check(x))
             , check(f(x)) -> f(check(x))
             , check(x) -> start(match(f(X()), x))
             , match(f(x), f(y)) -> f(match(x, y))
             , match(X(), x) -> proper(x)
             , proper(f(x)) -> f(proper(x))
             , f(ok(x)) -> ok(f(x))
             , f(found(x)) -> found(f(x))
             , active(f(x)) -> f(active(x))
             , f(mark(x)) -> mark(f(x))}
          Weak Trs:
            {  top(found(x)) -> top(active(x))
             , proper(c()) -> ok(c())
             , active(f(x)) -> mark(x)
             , top(active(c())) -> top(mark(c()))
             , start(ok(x)) -> found(x)}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^1))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component: {check(x) -> start(match(f(X()), x))}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
              Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
              Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
              Uargs(found) = {1}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             active(x1) = [1 0] x1 + [0]
                          [1 0]      [1]
             f(x1) = [1 0] x1 + [0]
                     [0 0]      [2]
             mark(x1) = [1 0] x1 + [0]
                        [0 0]      [1]
             top(x1) = [1 0] x1 + [0]
                       [1 0]      [1]
             c() = [0]
                   [0]
             check(x1) = [0 0] x1 + [1]
                         [1 0]      [2]
             start(x1) = [1 0] x1 + [0]
                         [0 0]      [1]
             match(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 1]      [0 1]      [1]
             X() = [0]
                   [0]
             proper(x1) = [0 0] x1 + [1]
                          [0 1]      [3]
             ok(x1) = [1 0] x1 + [0]
                      [0 0]      [1]
             found(x1) = [1 0] x1 + [0]
                         [0 0]      [1]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict Trs:
              {  top(mark(x)) -> top(check(x))
               , check(f(x)) -> f(check(x))
               , match(f(x), f(y)) -> f(match(x, y))
               , match(X(), x) -> proper(x)
               , proper(f(x)) -> f(proper(x))
               , f(ok(x)) -> ok(f(x))
               , f(found(x)) -> found(f(x))
               , active(f(x)) -> f(active(x))
               , f(mark(x)) -> mark(f(x))}
            Weak Trs:
              {  check(x) -> start(match(f(X()), x))
               , top(found(x)) -> top(active(x))
               , proper(c()) -> ok(c())
               , active(f(x)) -> mark(x)
               , top(active(c())) -> top(mark(c()))
               , start(ok(x)) -> found(x)}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^1))
          
          Proof:
            The weightgap principle applies, where following rules are oriented strictly:
            
            TRS Component: {top(mark(x)) -> top(check(x))}
            
            Interpretation of nonconstant growth:
            -------------------------------------
              The following argument positions are usable:
                Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
                Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
                Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
                Uargs(found) = {1}
              We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
              Interpretation Functions:
               active(x1) = [1 0] x1 + [0]
                            [0 1]      [0]
               f(x1) = [1 0] x1 + [0]
                       [0 0]      [2]
               mark(x1) = [1 0] x1 + [0]
                          [0 0]      [1]
               top(x1) = [1 2] x1 + [0]
                         [0 0]      [1]
               c() = [3]
                     [1]
               check(x1) = [1 0] x1 + [0]
                           [0 0]      [0]
               start(x1) = [1 0] x1 + [0]
                           [0 1]      [0]
               match(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                               [0 0]      [0 0]      [0]
               X() = [0]
                     [0]
               proper(x1) = [1 0] x1 + [1]
                            [0 1]      [3]
               ok(x1) = [1 0] x1 + [0]
                        [0 1]      [3]
               found(x1) = [1 0] x1 + [0]
                           [0 1]      [2]
            
            The strictly oriented rules are moved into the weak component.
            
            We consider the following Problem:
            
              Strict Trs:
                {  check(f(x)) -> f(check(x))
                 , match(f(x), f(y)) -> f(match(x, y))
                 , match(X(), x) -> proper(x)
                 , proper(f(x)) -> f(proper(x))
                 , f(ok(x)) -> ok(f(x))
                 , f(found(x)) -> found(f(x))
                 , active(f(x)) -> f(active(x))
                 , f(mark(x)) -> mark(f(x))}
              Weak Trs:
                {  top(mark(x)) -> top(check(x))
                 , check(x) -> start(match(f(X()), x))
                 , top(found(x)) -> top(active(x))
                 , proper(c()) -> ok(c())
                 , active(f(x)) -> mark(x)
                 , top(active(c())) -> top(mark(c()))
                 , start(ok(x)) -> found(x)}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: YES(?,O(n^1))
            
            Proof:
              The weightgap principle applies, where following rules are oriented strictly:
              
              TRS Component: {match(f(x), f(y)) -> f(match(x, y))}
              
              Interpretation of nonconstant growth:
              -------------------------------------
                The following argument positions are usable:
                  Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
                  Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
                  Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
                  Uargs(found) = {1}
                We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                Interpretation Functions:
                 active(x1) = [1 2] x1 + [0]
                              [0 0]      [0]
                 f(x1) = [1 0] x1 + [0]
                         [0 1]      [1]
                 mark(x1) = [1 2] x1 + [0]
                            [0 0]      [0]
                 top(x1) = [1 0] x1 + [0]
                           [0 0]      [1]
                 c() = [0]
                       [0]
                 check(x1) = [0 2] x1 + [0]
                             [0 0]      [3]
                 start(x1) = [1 0] x1 + [0]
                             [0 1]      [2]
                 match(x1, x2) = [0 0] x1 + [0 2] x2 + [0]
                                 [0 1]      [0 0]      [0]
                 X() = [0]
                       [0]
                 proper(x1) = [0 0] x1 + [0]
                              [0 0]      [3]
                 ok(x1) = [1 2] x1 + [0]
                          [0 0]      [2]
                 found(x1) = [1 2] x1 + [0]
                             [0 0]      [0]
              
              The strictly oriented rules are moved into the weak component.
              
              We consider the following Problem:
              
                Strict Trs:
                  {  check(f(x)) -> f(check(x))
                   , match(X(), x) -> proper(x)
                   , proper(f(x)) -> f(proper(x))
                   , f(ok(x)) -> ok(f(x))
                   , f(found(x)) -> found(f(x))
                   , active(f(x)) -> f(active(x))
                   , f(mark(x)) -> mark(f(x))}
                Weak Trs:
                  {  match(f(x), f(y)) -> f(match(x, y))
                   , top(mark(x)) -> top(check(x))
                   , check(x) -> start(match(f(X()), x))
                   , top(found(x)) -> top(active(x))
                   , proper(c()) -> ok(c())
                   , active(f(x)) -> mark(x)
                   , top(active(c())) -> top(mark(c()))
                   , start(ok(x)) -> found(x)}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(?,O(n^1))
              
              Proof:
                The weightgap principle applies, where following rules are oriented strictly:
                
                TRS Component: {match(X(), x) -> proper(x)}
                
                Interpretation of nonconstant growth:
                -------------------------------------
                  The following argument positions are usable:
                    Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
                    Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
                    Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
                    Uargs(found) = {1}
                  We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                  Interpretation Functions:
                   active(x1) = [1 0] x1 + [1]
                                [0 0]      [0]
                   f(x1) = [1 0] x1 + [0]
                           [0 0]      [0]
                   mark(x1) = [1 0] x1 + [1]
                              [0 0]      [0]
                   top(x1) = [1 0] x1 + [0]
                             [0 0]      [1]
                   c() = [0]
                         [0]
                   check(x1) = [0 0] x1 + [1]
                               [0 0]      [0]
                   start(x1) = [1 1] x1 + [0]
                               [0 0]      [0]
                   match(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                                   [0 1]      [0 0]      [0]
                   X() = [0]
                         [2]
                   proper(x1) = [0 0] x1 + [0]
                                [0 0]      [2]
                   ok(x1) = [1 0] x1 + [0]
                            [0 0]      [2]
                   found(x1) = [1 0] x1 + [1]
                               [0 0]      [0]
                
                The strictly oriented rules are moved into the weak component.
                
                We consider the following Problem:
                
                  Strict Trs:
                    {  check(f(x)) -> f(check(x))
                     , proper(f(x)) -> f(proper(x))
                     , f(ok(x)) -> ok(f(x))
                     , f(found(x)) -> found(f(x))
                     , active(f(x)) -> f(active(x))
                     , f(mark(x)) -> mark(f(x))}
                  Weak Trs:
                    {  match(X(), x) -> proper(x)
                     , match(f(x), f(y)) -> f(match(x, y))
                     , top(mark(x)) -> top(check(x))
                     , check(x) -> start(match(f(X()), x))
                     , top(found(x)) -> top(active(x))
                     , proper(c()) -> ok(c())
                     , active(f(x)) -> mark(x)
                     , top(active(c())) -> top(mark(c()))
                     , start(ok(x)) -> found(x)}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(?,O(n^1))
                
                Proof:
                  The weightgap principle applies, where following rules are oriented strictly:
                  
                  TRS Component: {check(f(x)) -> f(check(x))}
                  
                  Interpretation of nonconstant growth:
                  -------------------------------------
                    The following argument positions are usable:
                      Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
                      Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
                      Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
                      Uargs(found) = {1}
                    We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                    Interpretation Functions:
                     active(x1) = [1 1] x1 + [0]
                                  [0 0]      [2]
                     f(x1) = [1 0] x1 + [0]
                             [0 1]      [2]
                     mark(x1) = [1 1] x1 + [0]
                                [0 0]      [0]
                     top(x1) = [1 0] x1 + [0]
                               [0 0]      [1]
                     c() = [0]
                           [0]
                     check(x1) = [0 1] x1 + [0]
                                 [0 1]      [2]
                     start(x1) = [1 0] x1 + [0]
                                 [0 0]      [1]
                     match(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                     [0 1]      [0 0]      [0]
                     X() = [0]
                           [0]
                     proper(x1) = [0 0] x1 + [0]
                                  [0 0]      [0]
                     ok(x1) = [1 2] x1 + [0]
                              [0 0]      [0]
                     found(x1) = [1 2] x1 + [0]
                                 [0 0]      [0]
                  
                  The strictly oriented rules are moved into the weak component.
                  
                  We consider the following Problem:
                  
                    Strict Trs:
                      {  proper(f(x)) -> f(proper(x))
                       , f(ok(x)) -> ok(f(x))
                       , f(found(x)) -> found(f(x))
                       , active(f(x)) -> f(active(x))
                       , f(mark(x)) -> mark(f(x))}
                    Weak Trs:
                      {  check(f(x)) -> f(check(x))
                       , match(X(), x) -> proper(x)
                       , match(f(x), f(y)) -> f(match(x, y))
                       , top(mark(x)) -> top(check(x))
                       , check(x) -> start(match(f(X()), x))
                       , top(found(x)) -> top(active(x))
                       , proper(c()) -> ok(c())
                       , active(f(x)) -> mark(x)
                       , top(active(c())) -> top(mark(c()))
                       , start(ok(x)) -> found(x)}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(?,O(n^1))
                  
                  Proof:
                    The weightgap principle applies, where following rules are oriented strictly:
                    
                    TRS Component: {proper(f(x)) -> f(proper(x))}
                    
                    Interpretation of nonconstant growth:
                    -------------------------------------
                      The following argument positions are usable:
                        Uargs(active) = {}, Uargs(f) = {1}, Uargs(mark) = {1},
                        Uargs(top) = {1}, Uargs(check) = {}, Uargs(start) = {1},
                        Uargs(match) = {}, Uargs(proper) = {}, Uargs(ok) = {1},
                        Uargs(found) = {1}
                      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                      Interpretation Functions:
                       active(x1) = [1 2] x1 + [0]
                                    [0 0]      [3]
                       f(x1) = [1 0] x1 + [0]
                               [0 1]      [1]
                       mark(x1) = [1 2] x1 + [0]
                                  [0 0]      [0]
                       top(x1) = [1 0] x1 + [0]
                                 [0 0]      [1]
                       c() = [0]
                             [0]
                       check(x1) = [0 1] x1 + [0]
                                   [0 1]      [0]
                       start(x1) = [1 0] x1 + [0]
                                   [0 0]      [0]
                       match(x1, x2) = [0 0] x1 + [0 1] x2 + [0]
                                       [0 0]      [0 1]      [0]
                       X() = [0]
                             [0]
                       proper(x1) = [0 1] x1 + [0]
                                    [0 1]      [0]
                       ok(x1) = [1 2] x1 + [0]
                                [0 0]      [0]
                       found(x1) = [1 2] x1 + [0]
                                   [0 0]      [0]
                    
                    The strictly oriented rules are moved into the weak component.
                    
                    We consider the following Problem:
                    
                      Strict Trs:
                        {  f(ok(x)) -> ok(f(x))
                         , f(found(x)) -> found(f(x))
                         , active(f(x)) -> f(active(x))
                         , f(mark(x)) -> mark(f(x))}
                      Weak Trs:
                        {  proper(f(x)) -> f(proper(x))
                         , check(f(x)) -> f(check(x))
                         , match(X(), x) -> proper(x)
                         , match(f(x), f(y)) -> f(match(x, y))
                         , top(mark(x)) -> top(check(x))
                         , check(x) -> start(match(f(X()), x))
                         , top(found(x)) -> top(active(x))
                         , proper(c()) -> ok(c())
                         , active(f(x)) -> mark(x)
                         , top(active(c())) -> top(mark(c()))
                         , start(ok(x)) -> found(x)}
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(?,O(n^1))
                    
                    Proof:
                      We consider the following Problem:
                      
                        Strict Trs:
                          {  f(ok(x)) -> ok(f(x))
                           , f(found(x)) -> found(f(x))
                           , active(f(x)) -> f(active(x))
                           , f(mark(x)) -> mark(f(x))}
                        Weak Trs:
                          {  proper(f(x)) -> f(proper(x))
                           , check(f(x)) -> f(check(x))
                           , match(X(), x) -> proper(x)
                           , match(f(x), f(y)) -> f(match(x, y))
                           , top(mark(x)) -> top(check(x))
                           , check(x) -> start(match(f(X()), x))
                           , top(found(x)) -> top(active(x))
                           , proper(c()) -> ok(c())
                           , active(f(x)) -> mark(x)
                           , top(active(c())) -> top(mark(c()))
                           , start(ok(x)) -> found(x)}
                        StartTerms: basic terms
                        Strategy: innermost
                      
                      Certificate: YES(?,O(n^1))
                      
                      Proof:
                        The problem is match-bounded by 1.
                        The enriched problem is compatible with the following automaton:
                        {  active_0(3) -> 1
                         , active_0(5) -> 1
                         , active_0(9) -> 1
                         , active_0(11) -> 1
                         , active_0(12) -> 1
                         , f_0(3) -> 2
                         , f_0(5) -> 2
                         , f_0(9) -> 2
                         , f_0(11) -> 2
                         , f_0(12) -> 2
                         , f_1(3) -> 14
                         , f_1(5) -> 14
                         , f_1(9) -> 14
                         , f_1(11) -> 14
                         , f_1(12) -> 14
                         , f_1(17) -> 16
                         , mark_0(3) -> 3
                         , mark_0(5) -> 3
                         , mark_0(9) -> 3
                         , mark_0(11) -> 3
                         , mark_0(12) -> 3
                         , mark_1(14) -> 2
                         , mark_1(14) -> 14
                         , top_0(1) -> 4
                         , top_0(3) -> 4
                         , top_0(5) -> 4
                         , top_0(6) -> 4
                         , top_0(9) -> 4
                         , top_0(11) -> 4
                         , top_0(12) -> 4
                         , c_0() -> 5
                         , check_0(3) -> 6
                         , check_0(5) -> 6
                         , check_0(9) -> 6
                         , check_0(11) -> 6
                         , check_0(12) -> 6
                         , start_0(3) -> 7
                         , start_0(5) -> 7
                         , start_0(9) -> 7
                         , start_0(11) -> 7
                         , start_0(12) -> 7
                         , start_0(13) -> 6
                         , start_1(15) -> 6
                         , match_0(2, 3) -> 13
                         , match_0(2, 5) -> 13
                         , match_0(2, 9) -> 13
                         , match_0(2, 11) -> 13
                         , match_0(2, 12) -> 13
                         , match_0(3, 3) -> 8
                         , match_0(3, 5) -> 8
                         , match_0(3, 9) -> 8
                         , match_0(3, 11) -> 8
                         , match_0(3, 12) -> 8
                         , match_0(5, 3) -> 8
                         , match_0(5, 5) -> 8
                         , match_0(5, 9) -> 8
                         , match_0(5, 11) -> 8
                         , match_0(5, 12) -> 8
                         , match_0(9, 3) -> 8
                         , match_0(9, 5) -> 8
                         , match_0(9, 9) -> 8
                         , match_0(9, 11) -> 8
                         , match_0(9, 12) -> 8
                         , match_0(11, 3) -> 8
                         , match_0(11, 5) -> 8
                         , match_0(11, 9) -> 8
                         , match_0(11, 11) -> 8
                         , match_0(11, 12) -> 8
                         , match_0(12, 3) -> 8
                         , match_0(12, 5) -> 8
                         , match_0(12, 9) -> 8
                         , match_0(12, 11) -> 8
                         , match_0(12, 12) -> 8
                         , match_1(16, 3) -> 15
                         , match_1(16, 5) -> 15
                         , match_1(16, 9) -> 15
                         , match_1(16, 11) -> 15
                         , match_1(16, 12) -> 15
                         , X_0() -> 9
                         , X_1() -> 17
                         , proper_0(3) -> 8
                         , proper_0(3) -> 10
                         , proper_0(5) -> 8
                         , proper_0(5) -> 10
                         , proper_0(9) -> 8
                         , proper_0(9) -> 10
                         , proper_0(11) -> 8
                         , proper_0(11) -> 10
                         , proper_0(12) -> 8
                         , proper_0(12) -> 10
                         , ok_0(3) -> 11
                         , ok_0(5) -> 8
                         , ok_0(5) -> 10
                         , ok_0(5) -> 11
                         , ok_0(9) -> 11
                         , ok_0(11) -> 11
                         , ok_0(12) -> 11
                         , ok_1(14) -> 2
                         , ok_1(14) -> 14
                         , found_0(3) -> 7
                         , found_0(3) -> 12
                         , found_0(5) -> 7
                         , found_0(5) -> 12
                         , found_0(9) -> 7
                         , found_0(9) -> 12
                         , found_0(11) -> 7
                         , found_0(11) -> 12
                         , found_0(12) -> 7
                         , found_0(12) -> 12
                         , found_1(14) -> 2
                         , found_1(14) -> 14}

Hurray, we answered YES(?,O(n^1))