We consider the following Problem:

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

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

Proof:
  We consider the following Problem:
  
    Strict Trs: {h(f(x, y)) -> f(y, f(h(h(x)), a()))}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    We consider the following Problem:
    
      Strict Trs: {h(f(x, y)) -> f(y, f(h(h(x)), a()))}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      The problem is match-bounded by 2.
      The enriched problem is compatible with the following automaton:
      {  h_0(2) -> 1
       , h_1(2) -> 6
       , h_1(6) -> 4
       , h_2(2) -> 10
       , h_2(10) -> 8
       , f_0(2, 2) -> 2
       , f_1(2, 3) -> 1
       , f_1(2, 3) -> 6
       , f_1(2, 3) -> 10
       , f_1(4, 5) -> 3
       , f_2(3, 7) -> 4
       , f_2(3, 7) -> 8
       , f_2(8, 9) -> 7
       , a_0() -> 2
       , a_1() -> 5
       , a_2() -> 9}

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