 Prime-exponent encoding of a finite list

For a finite list $(a_0,\dots ,a_{r-1})$ of nonnegative integers, encode its length with the exponent of two and its entries with the following prime numbers: $2^r{\prod }_{j<r}{p}_{j+2}^{a_j+1}$, where $p_i$ is the $i$th prime number. Unique prime factorization recovers both the length and entries. Requiring positive exponents on exactly the prescribed consecutive primes also makes validity decidable. Nesting list descriptors therefore gives a Gödel encoding of deterministic finite automata and other finite syntactic objects.