Problem:
 a__h(X) -> a__g(mark(X),X)
 a__g(a(),X) -> a__f(b(),X)
 a__f(X,X) -> a__h(a__a())
 a__a() -> b()
 mark(h(X)) -> a__h(mark(X))
 mark(g(X1,X2)) -> a__g(mark(X1),X2)
 mark(a()) -> a__a()
 mark(f(X1,X2)) -> a__f(mark(X1),X2)
 mark(b()) -> b()
 a__h(X) -> h(X)
 a__g(X1,X2) -> g(X1,X2)
 a__a() -> a()
 a__f(X1,X2) -> f(X1,X2)

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [f](x0, x1) = 4x0 + x1 + 1,
   
   [g](x0, x1) = x0 + x1 + 1,
   
   [h](x0) = 5x0 + 1,
   
   [a__a] = 0,
   
   [a__f](x0, x1) = 4x0 + x1 + 1,
   
   [b] = 0,
   
   [a] = 0,
   
   [a__g](x0, x1) = x0 + x1 + 1,
   
   [mark](x0) = 4x0,
   
   [a__h](x0) = 5x0 + 1
  orientation:
   a__h(X) = 5X + 1 >= 5X + 1 = a__g(mark(X),X)
   
   a__g(a(),X) = X + 1 >= X + 1 = a__f(b(),X)
   
   a__f(X,X) = 5X + 1 >= 1 = a__h(a__a())
   
   a__a() = 0 >= 0 = b()
   
   mark(h(X)) = 20X + 4 >= 20X + 1 = a__h(mark(X))
   
   mark(g(X1,X2)) = 4X1 + 4X2 + 4 >= 4X1 + X2 + 1 = a__g(mark(X1),X2)
   
   mark(a()) = 0 >= 0 = a__a()
   
   mark(f(X1,X2)) = 16X1 + 4X2 + 4 >= 16X1 + X2 + 1 = a__f(mark(X1),X2)
   
   mark(b()) = 0 >= 0 = b()
   
   a__h(X) = 5X + 1 >= 5X + 1 = h(X)
   
   a__g(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 1 = g(X1,X2)
   
   a__a() = 0 >= 0 = a()
   
   a__f(X1,X2) = 4X1 + X2 + 1 >= 4X1 + X2 + 1 = f(X1,X2)
  problem:
   a__h(X) -> a__g(mark(X),X)
   a__g(a(),X) -> a__f(b(),X)
   a__f(X,X) -> a__h(a__a())
   a__a() -> b()
   mark(a()) -> a__a()
   mark(b()) -> b()
   a__h(X) -> h(X)
   a__g(X1,X2) -> g(X1,X2)
   a__a() -> a()
   a__f(X1,X2) -> f(X1,X2)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [f](x0, x1) = 4x0 + x1 + 1,
    
    [g](x0, x1) = x0 + x1 + 1,
    
    [h](x0) = 2x0,
    
    [a__a] = 0,
    
    [a__f](x0, x1) = 5x0 + x1 + 1,
    
    [b] = 0,
    
    [a] = 0,
    
    [a__g](x0, x1) = x0 + x1 + 1,
    
    [mark](x0) = x0,
    
    [a__h](x0) = 2x0 + 1
   orientation:
    a__h(X) = 2X + 1 >= 2X + 1 = a__g(mark(X),X)
    
    a__g(a(),X) = X + 1 >= X + 1 = a__f(b(),X)
    
    a__f(X,X) = 6X + 1 >= 1 = a__h(a__a())
    
    a__a() = 0 >= 0 = b()
    
    mark(a()) = 0 >= 0 = a__a()
    
    mark(b()) = 0 >= 0 = b()
    
    a__h(X) = 2X + 1 >= 2X = h(X)
    
    a__g(X1,X2) = X1 + X2 + 1 >= X1 + X2 + 1 = g(X1,X2)
    
    a__a() = 0 >= 0 = a()
    
    a__f(X1,X2) = 5X1 + X2 + 1 >= 4X1 + X2 + 1 = f(X1,X2)
   problem:
    a__h(X) -> a__g(mark(X),X)
    a__g(a(),X) -> a__f(b(),X)
    a__f(X,X) -> a__h(a__a())
    a__a() -> b()
    mark(a()) -> a__a()
    mark(b()) -> b()
    a__g(X1,X2) -> g(X1,X2)
    a__a() -> a()
    a__f(X1,X2) -> f(X1,X2)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [f](x0, x1) = 2x0 + x1 + 2,
     
     [g](x0, x1) = x0 + x1,
     
     [a__a] = 0,
     
     [a__f](x0, x1) = 4x0 + x1 + 2,
     
     [b] = 0,
     
     [a] = 0,
     
     [a__g](x0, x1) = 2x0 + x1 + 2,
     
     [mark](x0) = x0,
     
     [a__h](x0) = 3x0 + 2
    orientation:
     a__h(X) = 3X + 2 >= 3X + 2 = a__g(mark(X),X)
     
     a__g(a(),X) = X + 2 >= X + 2 = a__f(b(),X)
     
     a__f(X,X) = 5X + 2 >= 2 = a__h(a__a())
     
     a__a() = 0 >= 0 = b()
     
     mark(a()) = 0 >= 0 = a__a()
     
     mark(b()) = 0 >= 0 = b()
     
     a__g(X1,X2) = 2X1 + X2 + 2 >= X1 + X2 = g(X1,X2)
     
     a__a() = 0 >= 0 = a()
     
     a__f(X1,X2) = 4X1 + X2 + 2 >= 2X1 + X2 + 2 = f(X1,X2)
    problem:
     a__h(X) -> a__g(mark(X),X)
     a__g(a(),X) -> a__f(b(),X)
     a__f(X,X) -> a__h(a__a())
     a__a() -> b()
     mark(a()) -> a__a()
     mark(b()) -> b()
     a__a() -> a()
     a__f(X1,X2) -> f(X1,X2)
    Matrix Interpretation Processor: dim=1
     
     interpretation:
      [f](x0, x1) = 4x0 + x1,
      
      [a__a] = 0,
      
      [a__f](x0, x1) = 6x0 + x1 + 1,
      
      [b] = 0,
      
      [a] = 0,
      
      [a__g](x0, x1) = x0 + x1 + 1,
      
      [mark](x0) = 6x0,
      
      [a__h](x0) = 7x0 + 1
     orientation:
      a__h(X) = 7X + 1 >= 7X + 1 = a__g(mark(X),X)
      
      a__g(a(),X) = X + 1 >= X + 1 = a__f(b(),X)
      
      a__f(X,X) = 7X + 1 >= 1 = a__h(a__a())
      
      a__a() = 0 >= 0 = b()
      
      mark(a()) = 0 >= 0 = a__a()
      
      mark(b()) = 0 >= 0 = b()
      
      a__a() = 0 >= 0 = a()
      
      a__f(X1,X2) = 6X1 + X2 + 1 >= 4X1 + X2 = f(X1,X2)
     problem:
      a__h(X) -> a__g(mark(X),X)
      a__g(a(),X) -> a__f(b(),X)
      a__f(X,X) -> a__h(a__a())
      a__a() -> b()
      mark(a()) -> a__a()
      mark(b()) -> b()
      a__a() -> a()
     Unfolding Processor:
      loop length: 7
      terms:
       a__g(mark(a__a()),b())
       a__g(mark(a()),b())
       a__g(a__a(),b())
       a__g(a(),b())
       a__f(b(),b())
       a__h(a__a())
       a__g(mark(a__a()),a__a())
      context: []
      substitution:
       
      Qed