:: deftheorem Def21 defines PTClasses OSAFREE:def 21 :
for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for b₃ being Function of (TS (DTConOSA X)),(bool [:(TS (DTConOSA X)), the carrier of S:]) holds
( b₃ = PTClasses X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b₃ . (root-tree t) = @ t ) & ( for nt being Symbol of (DTConOSA X)
for ts being FinSequence of TS (DTConOSA X) st nt ==> roots ts holds
b₃ . (nt -tree ts) = @ (nt,(b₃ * ts)) ) ) );