Many programs process lists by recursing in a wide variety of sequential and/or divide-and-conquer patterns.
Reasoning about the correctness and completeness of these programs requires reasoning about the lengths of
the lists, techniques for which are typically undecidable or at least NP-complete. In this paper we show how
introducing a relatively simple (sub-)language for expressions describing list lengths, whilst not completely
general, covers a great number of these patterns. It includes not only doubling but also exponentiation (iterated
doubling), and moreover admits a simple length-checking algorithm that is complete over a predictable problem
domain. We prove termination of the algorithm via category-theoretic pullbacks, formalized in Agda, as well as
providing a more realistic implementation in Rocq, and a toy language Fulbourn with interpreter in Haskell.