for G being non empty DTConstrStr
for n, m being String of G st n ==> m holds
m is_derivable_from n