========================================== reduce in TEST : ?(((P(x:S) -> G(x:S)), (empty -> P(f-x'(x:S))), (P(x:S) -> P( f-x''(x:S)), Q(x:S)), (P(x:S) -> Q(x:S), Q(f-x''(x:S))), (U(x:S) -> R( x:S)), (P(x:S) -> U(x:S)), (G(x:S), U(x:S) -> empty), (P(x:S), Q(x:S) -> empty))) . rewrites: 3020 in 29ms cpu (29ms real) (100680 rewrites/second) result State: [ ("G",'_->_['empty.AtomMagma,'G['f-x'['V#1:S]]],empty -> G(f-x'(V#1:S))), ( "G",'_->_['G['f-x'['V#1:S]],'empty.AtomMagma],G(f-x'(V#1:S)) -> empty), ( "P",'_->_['empty.AtomMagma,'P['f-x'['x:S]]],empty -> P(f-x'(x:S))), ("P", '_->_['P['V#1:S],'R['V#1:S]],P(V#1:S) -> R(V#1:S)), ("P",'_->_['P['x:S],'G[ 'x:S]],P(x:S) -> G(x:S)), ("P",'_->_['P['x:S],'U['x:S]],P(x:S) -> U(x:S)), ("R",'_->_['empty.AtomMagma,'R['f-x'['V#1:S]]],empty -> R(f-x'(V#1:S))), ( "R",'_->_['P['V#1:S],'R['V#1:S]],P(V#1:S) -> R(V#1:S)), ("U",'_->_[ 'empty.AtomMagma,'U['f-x'['V#1:S]]],empty -> U(f-x'(V#1:S))), ("U",'_->_[ 'P['x:S],'U['x:S]],P(x:S) -> U(x:S)), ("U",'_->_['U['x:S],'R['x:S]],U(x:S) -> R(x:S)), ("U",'_->_['_`,_['G['x:S],'U['x:S]],'empty.AtomMagma],G(x:S), U(x:S) -> empty), "G" : (empty -> G(f-x'(V#1:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[ G(f-x'(V#1:S))], "G" : (G(f-x'(V#1:S)) -> empty) |-> empty, "P" : (empty -> P(f-x'(x:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[P(f-x'(x:S))], "P" : (P(x:S) -> G(x:S)) |-> empty, "R" : (empty -> R(f-x'(V#1:S))) |-> (( empty).AtomMagma -> (empty).AtomMagma)[R(f-x'(V#1:S))], "R" : (P(V#1:S) -> R(V#1:S)) |-> (P(V#1:S) -> (empty).AtomMagma)[R(V#1:S)], "U" : (empty -> U( f-x'(V#1:S))) |-> ((empty).AtomMagma -> (empty).AtomMagma)[U(f-x'(V#1:S))], "U" : (P(x:S) -> U(x:S)) |-> (P(x:S) -> (empty).AtomMagma)[U(x:S)], "U" : ( U(x:S) -> R(x:S)) |-> empty, "U" : (G(x:S), U(x:S) -> empty) |-> empty, "G" : (G(f-x'(V#1:S)) -> empty) |-> ([G(f-x'(V#1:S))]empty -> empty), "P" : ( P(x:S) -> G(x:S)) |-> ([P(x:S)]empty -> G(x:S)), "P" : (P(x:S) -> U(x:S)) |-> ([P(x:S)]empty -> U(x:S)), "P" : (P(V#1:S) -> R(V#1:S)) |-> ([P( V#1:S)]empty -> R(V#1:S)), "U" : (U(x:S) -> R(x:S)) |-> ([U(x:S)]empty -> R(x:S)), "U" : (G(x:S), U(x:S) -> empty) |-> ([U(x:S)]G(x:S) -> empty), empty -> empty, 9 ] Bye.