:: deftheorem defines NHReverse OSAFREE:def 29 :
for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for s being Element of S
for b₄ being Function of (OSFreeGen (s,X)),(PTVars (s,X)) holds
( b₄ = NHReverse (s,X) iff for t being Symbol of (DTConOSA X) st ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t) in OSFreeGen (s,X) holds
b₄ . (((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree t)) = root-tree t );