*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        g(f(x),y) -> f(h(x,y))
        h(x,y) -> g(x,f(y))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {g/2,h/2} / {f/1}
      Obligation:
        Full
        basic terms: {g,h}/{f}
    Applied Processor:
      ToInnermost
    Proof:
      switch to innermost, as the system is overlay and right linear and does not contain weak rules
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        g(f(x),y) -> f(h(x,y))
        h(x,y) -> g(x,f(y))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {g/2,h/2} / {f/1}
      Obligation:
        Innermost
        basic terms: {g,h}/{f}
    Applied Processor:
      NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation:
      The following argument positions are considered usable:
        uargs(f) = {1}
      
      Following symbols are considered usable:
        {g,h}
      TcT has computed the following interpretation:
        p(f) = [1] x1 + [2]
        p(g) = [8] x1 + [0]
        p(h) = [8] x1 + [1]
      
      Following rules are strictly oriented:
      g(f(x),y) = [8] x + [16]
                > [8] x + [3] 
                = f(h(x,y))   
      
         h(x,y) = [8] x + [1] 
                > [8] x + [0] 
                = g(x,f(y))   
      
      
      Following rules are (at-least) weakly oriented:
      
*** 1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        g(f(x),y) -> f(h(x,y))
        h(x,y) -> g(x,f(y))
      Signature:
        {g/2,h/2} / {f/1}
      Obligation:
        Innermost
        basic terms: {g,h}/{f}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).