(from AG01 4.31) (VAR x) (RULES a(d(x)) -> d(c(b(a(x)))) b(c(x)) -> c(d(a(b(x)))) a(c(x)) -> x b(d(x)) -> x ) (STRATEGY INNERMOST)
Submit to AProVE Web Frontend
Edit in AProVE Web Frontend