theorem :: DTCONSTR:18

for nt being Symbol of PeanoNat holds
( ( nt = 0 implies PostTraversalLanguage nt = {<*0*>} ) & ( nt = 1 implies PostTraversalLanguage nt = { (<*0*> ^ (n |-> 1)) where n is Element of NAT : n <> 0 } ) )