Prime-exponent encoding of a finite list (source code)

= Prime-exponent encoding of a finite list
{title2=$2^r\prod_{j<r}p_{j+2}^{a_j+1}$}

For a finite list $(a_0,\ldots,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.