MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   a(b(x)) -> b(b(a(a(x))))
  weak:
   
  Open