MAYBE

Problem:
 a(f(),0()) -> a(s(),0())
 a(d(),0()) -> 0()
 a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x)))))
 a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x))))
 a(p(),a(s(),x)) -> x

Proof:
 RT Transformation Processor:
  strict:
   a(f(),0()) -> a(s(),0())
   a(d(),0()) -> 0()
   a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x)))))
   a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x))))
   a(p(),a(s(),x)) -> x
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   interpretation:
    [p] = 5,
    
    [d] = 25,
    
    [s] = 0,
    
    [a](x0, x1) = x0 + x1 + 4,
    
    [0] = 0,
    
    [f] = 16
   orientation:
    a(f(),0()) = 20 >= 4 = a(s(),0())
    
    a(d(),0()) = 29 >= 0 = 0()
    
    a(d(),a(s(),x)) = x + 33 >= x + 50 = a(s(),a(s(),a(d(),a(p(),a(s(),x)))))
    
    a(f(),a(s(),x)) = x + 24 >= x + 62 = a(d(),a(f(),a(p(),a(s(),x))))
    
    a(p(),a(s(),x)) = x + 13 >= x = x
   problem:
    strict:
     a(d(),a(s(),x)) -> a(s(),a(s(),a(d(),a(p(),a(s(),x)))))
     a(f(),a(s(),x)) -> a(d(),a(f(),a(p(),a(s(),x))))
    weak:
     a(f(),0()) -> a(s(),0())
     a(d(),0()) -> 0()
     a(p(),a(s(),x)) -> x
   Open