========================================== reduce in TEST : ?(((empty -> P(x:S, y:S)), (P(f-x'(x:S, y:S), f-y'(x:S, y:S)) -> empty))) . rewrites: 424 in 26ms cpu (26ms real) (15706 rewrites/second) result State: [ ("P",'_->_['empty.AtomMagma,'P['x:S,'y:S]],empty -> P(x:S, y:S)), ("P",'_->_[ 'P['f-x'['x:S,'y:S],'f-y'['x:S,'y:S]],'empty.AtomMagma],P(f-x'(x:S, y:S), f-y'(x:S, y:S)) -> empty), "P" : (empty -> P(x:S, y:S)) |-> ((empty).AtomMagma -> (empty).AtomMagma)[P( x:S, y:S)], "P" : (P(f-x'(x:S, y:S), f-y'(x:S, y:S)) -> empty) |-> empty, "P" : (P(f-x'(x:S, y:S), f-y'(x:S, y:S)) -> empty) |-> ([P(f-x'(x:S, y:S), f-y'(x:S, y:S))]empty -> empty), empty -> empty, 1 ] Bye.