MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   f(a()) -> f(a())
   a() -> b()
  weak:
   
  Arctic Interpretation Processor:
   dimension: 3
   interpretation:
          [0 ]
    [b] = [-&]
          [-&],
    
              [0 0 0]  
    [f](x0) = [0 0 0]x0
              [0 0 0]  ,
    
          [1]
    [a] = [0]
          [0]
   orientation:
             [1]    [1]         
    f(a()) = [1] >= [1] = f(a())
             [1]    [1]         
    
          [1]    [0 ]      
    a() = [0] >= [-&] = b()
          [0]    [-&]      
   problem:
    strict:
     f(a()) -> f(a())
    weak:
     a() -> b()
   Open