MAYBE

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

Proof:
 RT Transformation Processor:
  strict:
   a(f(),a(g(),a(f(),x))) -> a(f(),a(g(),a(g(),a(f(),x))))
   a(g(),a(f(),a(g(),x))) -> a(g(),a(f(),a(f(),a(g(),x))))
  weak:
   
  Open