:: deftheorem Def31 defines PTMin OSAFREE:def 31 :
for S being monotone regular locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being Function of (TS (DTConOSA X)),(TS (DTConOSA X)) holds
( b₃ = PTMin X iff ( ( for t being Symbol of (DTConOSA X) st t in Terminals (DTConOSA X) holds
b₃ . (root-tree t) = pi 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) = pi ((@ (X,nt)),(b₃ * ts)) ) ) );