:: deftheorem Def17 defines Reverse MSAFREE:def 17 :
for S being non empty non void ManySortedSign
for X being V5() ManySortedSet of the carrier of S
for s being SortSymbol of S
for b₄ being Function of (FreeGen (s,X)),(X . s) holds
( b₄ = Reverse (s,X) iff for t being Symbol of (DTConMSA X) st root-tree t in FreeGen (s,X) holds
b₄ . (root-tree t) = t `1 );