:: deftheorem Def16 defines pi OSAFREE:def 16 :
for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
pi t = root-tree t;