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