We consider the following Problem:

  Strict Trs:
    {  f(a()) -> g(h(a()))
     , h(g(x)) -> g(h(f(x)))
     , k(x, h(x), a()) -> h(x)
     , k(f(x), y, x) -> f(x)}
  StartTerms: basic terms
  Strategy: innermost

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

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  f(a()) -> g(h(a()))
       , h(g(x)) -> g(h(f(x)))
       , k(x, h(x), a()) -> h(x)
       , k(f(x), y, x) -> 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:
      {  k(x, h(x), a()) -> h(x)
       , k(f(x), y, x) -> f(x)}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(f) = {}, Uargs(g) = {1}, Uargs(h) = {1}, Uargs(k) = {}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       f(x1) = [0 0] x1 + [1]
               [0 0]      [1]
       a() = [0]
             [0]
       g(x1) = [1 0] x1 + [1]
               [0 0]      [1]
       h(x1) = [1 0] x1 + [0]
               [0 0]      [1]
       k(x1, x2, x3) = [1 1] x1 + [0 0] x2 + [1 1] x3 + [1]
                       [0 0]      [0 0]      [0 0]      [1]
    
    The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  f(a()) -> g(h(a()))
         , h(g(x)) -> g(h(f(x)))}
      Weak Trs:
        {  k(x, h(x), a()) -> h(x)
         , k(f(x), y, x) -> 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: {f(a()) -> g(h(a()))}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(f) = {}, Uargs(g) = {1}, Uargs(h) = {1}, Uargs(k) = {}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         f(x1) = [0 0] x1 + [1]
                 [0 0]      [1]
         a() = [0]
               [0]
         g(x1) = [1 0] x1 + [0]
                 [0 0]      [1]
         h(x1) = [1 0] x1 + [0]
                 [1 0]      [1]
         k(x1, x2, x3) = [1 0] x1 + [0 0] x2 + [1 0] x3 + [1]
                         [0 1]      [0 1]      [1 1]      [0]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs: {h(g(x)) -> g(h(f(x)))}
        Weak Trs:
          {  f(a()) -> g(h(a()))
           , k(x, h(x), a()) -> h(x)
           , k(f(x), y, x) -> f(x)}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        We fail transforming the problem using 'weightgap of dimension Nat 2, maximal degree 1, cbits 4'
        
          The weightgap principle does not apply
        
        We try instead 'weightgap of dimension Nat 3, maximal degree 2, cbits 3' on the problem
        
        Strict Trs: {h(g(x)) -> g(h(f(x)))}
        Weak Trs:
          {  f(a()) -> g(h(a()))
           , k(x, h(x), a()) -> h(x)
           , k(f(x), y, x) -> f(x)}
        StartTerms: basic terms
        Strategy: innermost
        
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component: {h(g(x)) -> g(h(f(x)))}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(f) = {}, Uargs(g) = {1}, Uargs(h) = {1}, Uargs(k) = {}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             f(x1) = [0 2 0] x1 + [0]
                     [0 0 0]      [0]
                     [1 0 0]      [0]
             a() = [1]
                   [2]
                   [0]
             g(x1) = [1 2 0] x1 + [0]
                     [0 0 0]      [0]
                     [0 0 0]      [1]
             h(x1) = [1 0 1] x1 + [0]
                     [0 0 0]      [0]
                     [0 0 0]      [2]
             k(x1, x2, x3) = [1 0 0] x1 + [1 0 0] x2 + [0 0 0] x3 + [1]
                             [0 0 0]      [0 0 0]      [0 0 0]      [1]
                             [0 0 1]      [0 0 0]      [0 0 1]      [2]
          
          The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Weak Trs:
            {  h(g(x)) -> g(h(f(x)))
             , f(a()) -> g(h(a()))
             , k(x, h(x), a()) -> h(x)
             , k(f(x), y, x) -> f(x)}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(O(1),O(1))
        
        Proof:
          We consider the following Problem:
          
            Weak Trs:
              {  h(g(x)) -> g(h(f(x)))
               , f(a()) -> g(h(a()))
               , k(x, h(x), a()) -> h(x)
               , k(f(x), y, x) -> f(x)}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(O(1),O(1))
          
          Proof:
            Empty rules are trivially bounded

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