:: deftheorem Def8 defines PN-to-NAT DTCONSTR:def 8 :
for b₁ being Function of (TS PeanoNat),NAT holds
( b₁ = PN-to-NAT iff ( ( for t being Symbol of PeanoNat st t in Terminals PeanoNat holds
b₁ . (root-tree t) = 0 ) & ( for nt being Symbol of PeanoNat
for ts being FinSequence of TS PeanoNat st nt ==> roots ts holds
b₁ . (nt -tree ts) = plus-one (b₁ * ts) ) ) );