========================================== reduce in TEST : !(((empty -> L(f-x'''(x:S, x':S))), (L(x':S), R(x:S) -> M( x':S)), (empty -> P(f-x'''(x:S, x':S))), (P(x:S) -> Q(x':S)), (R(f-x''(x:S, x':S)) -> Q(f-x''(x:S, x':S))), (M(f-x'''(x:S, x':S)) -> empty), (Q(f-x''( x:S, x':S)) -> R(f-x''(x:S, x':S))))) . rewrites: 2870 in 30ms cpu (30ms real) (92592 rewrites/second) result State: [empty -> empty,9] Bye.