:: deftheorem Def11 defines pnptree LTLAXIO4:def 11 :
for P being PNPair
for b₂ being finite-branching DecoratedTree of [:(LTLB_WFF **),(LTLB_WFF **):] holds
( b₂ is pnptree of P iff ( b₂ . {} = P & ( for t being Element of dom b₂
for w being Element of [:(LTLB_WFF **),(LTLB_WFF **):] st w = b₂ . t holds
succ (b₂,t) = the Enumeration of compn w ) ) );