MAYBE

Problem:
 f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
 f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))

Proof:
 RT Transformation Processor:
  strict:
   f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
   f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [f](x0, x1) = x0 + x1,
    
    [b] = 0,
    
    [a] = 20
   orientation:
    f(a(),f(b(),x)) = x + 20 >= x + 60 = f(a(),f(a(),f(a(),x)))
    
    f(b(),f(a(),x)) = x + 20 >= x = f(b(),f(b(),f(b(),x)))
   problem:
    strict:
     f(a(),f(b(),x)) -> f(a(),f(a(),f(a(),x)))
    weak:
     f(b(),f(a(),x)) -> f(b(),f(b(),f(b(),x)))
   Open