Problem:
 f(x,x) -> f(i(x),g(g(x)))
 f(x,y) -> x
 g(x) -> i(x)
 f(x,i(x)) -> f(x,x)
 f(i(x),i(g(x))) -> a()

Proof:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [a] = 2,
   
   [g](x0) = x0,
   
   [i](x0) = x0,
   
   [f](x0, x1) = 2x0 + 2x1 + 2
  orientation:
   f(x,x) = 4x + 2 >= 4x + 2 = f(i(x),g(g(x)))
   
   f(x,y) = 2x + 2y + 2 >= x = x
   
   g(x) = x >= x = i(x)
   
   f(x,i(x)) = 4x + 2 >= 4x + 2 = f(x,x)
   
   f(i(x),i(g(x))) = 4x + 2 >= 2 = a()
  problem:
   f(x,x) -> f(i(x),g(g(x)))
   g(x) -> i(x)
   f(x,i(x)) -> f(x,x)
   f(i(x),i(g(x))) -> a()
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [a] = 0,
    
    [g](x0) = x0,
    
    [i](x0) = x0,
    
    [f](x0, x1) = x0 + x1 + 5
   orientation:
    f(x,x) = 2x + 5 >= 2x + 5 = f(i(x),g(g(x)))
    
    g(x) = x >= x = i(x)
    
    f(x,i(x)) = 2x + 5 >= 2x + 5 = f(x,x)
    
    f(i(x),i(g(x))) = 2x + 5 >= 0 = a()
   problem:
    f(x,x) -> f(i(x),g(g(x)))
    g(x) -> i(x)
    f(x,i(x)) -> f(x,x)
   Unfolding Processor:
    loop length: 4
    terms:
     f(x92,x92)
     f(i(x92),g(g(x92)))
     f(i(x92),i(g(x92)))
     f(i(x92),i(i(x92)))
    context: []
    substitution:
     x92 -> i(x92)
    Qed