We identify a class of programs manipulating lists of data items for which
checking functional equivalence and pre/post verification conditions is
decidable. Lists are modeled as data words, (unbounded) sequences of data
values, tagged with symbols from a finite set, over a potentially infinite data
domain that supports only the operations of equality and ordering. First, we
introduce streaming data-word transducers that map input data words to output
data words in a single left-to-right pass in linear time.