========================================== reduce in TEST : ?(((empty -> G(x:S), H(x:S)), (empty -> G(x:S), P(x:S)), ( empty -> H(x:S), U(x:S)), (empty -> P(x:S), U(x:S)), (G(x:S), H(x:S) -> empty), (U(f-x'(x:S)) -> empty), (H(x:S), P(x:S) -> empty))) . rewrites: 3277 in 31ms cpu (32ms real) (102422 rewrites/second) result State: [ ("G",'_->_['empty.AtomMagma,'G['V#1:S]],empty -> G(V#1:S)), ("G",'_->_['G[ 'f-x'['V#1:S]],'empty.AtomMagma],G(f-x'(V#1:S)) -> empty), ("H",'_->_[ 'empty.AtomMagma,'H['f-x'['V#1:S]]],empty -> H(f-x'(V#1:S))), ("H",'_->_[ '_`,_['G['x:S],'H['x:S]],'empty.AtomMagma],G(x:S), H(x:S) -> empty), ("P", '_->_['empty.AtomMagma,'P['f-x'['V#1:S]]],empty -> P(f-x'(V#1:S))), ("P", '_->_['_`,_['H['x:S],'P['x:S]],'empty.AtomMagma],H(x:S), P(x:S) -> empty), ("U",'_->_['empty.AtomMagma,'_`,_['H['x:S],'U['x:S]]],empty -> H(x:S), U( x:S)), ("U",'_->_['empty.AtomMagma,'_`,_['P['x:S],'U['x:S]]],empty -> P( x:S), U(x:S)), ("U",'_->_['U['f-x'['x:S]],'empty.AtomMagma],U(f-x'(x:S)) -> empty), "G" : (empty -> G(V#1:S)) |-> ((empty).AtomMagma -> (empty).AtomMagma)[G( V#1:S)], "G" : (G(f-x'(V#1:S)) -> empty) |-> empty, "H" : (empty -> H(f-x'( V#1:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[H(f-x'(V#1:S))], "H" : (G(x:S), H(x:S) -> empty) |-> empty, "P" : (empty -> P(f-x'(V#1:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[P(f-x'(V#1:S))], "P" : (H(x:S), P( x:S) -> empty) |-> empty, "U" : (empty -> H(x:S), U(x:S)) |-> (( empty).AtomMagma -> H(x:S))[U(x:S)], "U" : (empty -> P(x:S), U(x:S)) |-> (( empty).AtomMagma -> P(x:S))[U(x:S)], "U" : (U(f-x'(x:S)) -> empty) |-> empty, "G" : (G(f-x'(V#1:S)) -> empty) |-> ([G(f-x'(V#1:S))]empty -> empty), "H" : ( G(x:S), H(x:S) -> empty) |-> ([H(x:S)]G(x:S) -> empty), "P" : (H(x:S), P( x:S) -> empty) |-> ([P(x:S)]H(x:S) -> empty), "U" : (U(f-x'(x:S)) -> empty) |-> ([U(f-x'(x:S))]empty -> empty), empty -> empty, 11 ] Bye.