========================================== reduce in TEST : ?(((empty -> P, Q(x:S), Q(x':S)), (P -> empty), (Q(f-x''(x:S, x':S)) -> empty))) . rewrites: 1380 in 23ms cpu (23ms real) (57507 rewrites/second) result State: [ ("P",'_->_['P.Atom,'empty.AtomMagma],P -> empty), ("P",'_->_[ 'empty.AtomMagma,'P.Atom],empty -> P), ("Q",'_->_['Q['f-x''['x:S,'x':S]], 'empty.AtomMagma],Q(f-x''(x:S, x':S)) -> empty), "P" : (empty -> P) |-> ((empty).AtomMagma -> (empty).AtomMagma)[P], "P" : (P -> empty) |-> empty, "Q" : (Q(f-x''(x:S, x':S)) -> empty) |-> empty, "P" : (P -> empty) |-> ([P]empty -> empty), "Q" : (Q(f-x''(x:S, x':S)) -> empty) |-> ([Q(f-x''(x:S, x':S))]empty -> empty), empty -> empty, 3 ] Bye.