MAYBE

Problem:
 a(lambda(x),y) -> lambda(a(x,1()))
 a(lambda(x),y) -> lambda(a(x,a(y,t())))
 a(a(x,y),z) -> a(x,a(y,z))
 lambda(x) -> x
 a(x,y) -> x
 a(x,y) -> y

Proof:
 RT Transformation Processor:
  strict:
   a(lambda(x),y) -> lambda(a(x,1()))
   a(lambda(x),y) -> lambda(a(x,a(y,t())))
   a(a(x,y),z) -> a(x,a(y,z))
   lambda(x) -> x
   a(x,y) -> x
   a(x,y) -> y
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [t] = 6,
    
    [1] = 29,
    
    [a](x0, x1) = x0 + x1 + 9,
    
    [lambda](x0) = x0 + 18
   orientation:
    a(lambda(x),y) = x + y + 27 >= x + 56 = lambda(a(x,1()))
    
    a(lambda(x),y) = x + y + 27 >= x + y + 42 = lambda(a(x,a(y,t())))
    
    a(a(x,y),z) = x + y + z + 18 >= x + y + z + 18 = a(x,a(y,z))
    
    lambda(x) = x + 18 >= x = x
    
    a(x,y) = x + y + 9 >= x = x
    
    a(x,y) = x + y + 9 >= y = y
   problem:
    strict:
     a(lambda(x),y) -> lambda(a(x,1()))
     a(lambda(x),y) -> lambda(a(x,a(y,t())))
     a(a(x,y),z) -> a(x,a(y,z))
    weak:
     lambda(x) -> x
     a(x,y) -> x
     a(x,y) -> y
   Open