========================================== reduce in TEST : ?(((R(x:S) -> H(x:S)), (H(x:S), Q(x:S) -> J(x:S)), (empty -> P(f-x'(x:S))), (P(x:S), G(x:S) -> Q(x:S)), (H(x:S), P(x:S) -> Q(x:S)), ( empty -> R(f-x'(x:S))), (J(f-x'(x:S)) -> empty))) . rewrites: 3596 in 35ms cpu (36ms real) (99902 rewrites/second) result State: [ ("H",'_->_['empty.AtomMagma,'H['f-x'['V#1:S]]],empty -> H(f-x'(V#1:S))), ( "J",'_->_['empty.AtomMagma,'J['f-x'['V#1:S]]],empty -> J(f-x'(V#1:S))), ( "J",'_->_['J['f-x'['x:S]],'empty.AtomMagma],J(f-x'(x:S)) -> empty), ("P", '_->_['empty.AtomMagma,'P['f-x'['x:S]]],empty -> P(f-x'(x:S))), ("P",'_->_[ '_`,_['H['x:S],'P['x:S]],'Q['x:S]],H(x:S), P(x:S) -> Q(x:S)), ("Q",'_->_[ 'empty.AtomMagma,'Q['f-x'['V#1:S]]],empty -> Q(f-x'(V#1:S))), ("Q",'_->_[ '_`,_['H['x:S],'P['x:S]],'Q['x:S]],H(x:S), P(x:S) -> Q(x:S)), ("Q",'_->_[ '_`,_['H['x:S],'Q['x:S]],'J['x:S]],H(x:S), Q(x:S) -> J(x:S)), ("R",'_->_[ 'empty.AtomMagma,'R['f-x'['x:S]]],empty -> R(f-x'(x:S))), ("R",'_->_['R[ 'x:S],'H['x:S]],R(x:S) -> H(x:S)), "H" : (empty -> H(f-x'(V#1:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[ H(f-x'(V#1:S))], "J" : (empty -> J(f-x'(V#1:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[J(f-x'(V#1:S))], "J" : (J(f-x'(x:S)) -> empty) |-> empty, "P" : (empty -> P(f-x'(x:S))) |-> ((empty).AtomMagma -> ( empty).AtomMagma)[P(f-x'(x:S))], "Q" : (empty -> Q(f-x'(V#1:S))) |-> (( empty).AtomMagma -> (empty).AtomMagma)[Q(f-x'(V#1:S))], "Q" : (H(x:S), Q( x:S) -> J(x:S)) |-> empty, "Q" : (H(x:S), P(x:S) -> Q(x:S)) |-> (H(x:S), P( x:S) -> (empty).AtomMagma)[Q(x:S)], "R" : (empty -> R(f-x'(x:S))) |-> (( empty).AtomMagma -> (empty).AtomMagma)[R(f-x'(x:S))], "R" : (R(x:S) -> H( x:S)) |-> empty, "J" : (J(f-x'(x:S)) -> empty) |-> ([J(f-x'(x:S))]empty -> empty), "P" : (H( x:S), P(x:S) -> Q(x:S)) |-> ([P(x:S)]H(x:S) -> Q(x:S)), "Q" : (H(x:S), Q( x:S) -> J(x:S)) |-> ([Q(x:S)]H(x:S) -> J(x:S)), "R" : (R(x:S) -> H(x:S)) |-> ([R(x:S)]empty -> H(x:S)), empty -> empty, 10 ] Bye.