/home/nowonder/forschung/aprove/TPDB05/TRS/HofWald/7.trs

The program

( Comment see Dieter Probst, Thomas Studer:
  http://www.iam.unibe.ch/~tstuder/papers/j.pdf )

( VAR a b c d )
( RULES f(f(f(f(j,a),b),c),d) -> f(f(a,b),f(f(a,d),c)) )

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend