call $e_i$ the *exponent* of $\gamma_i$, and we refer to $\tau_0\gamma_1\tau_1\ldots\gamma_k\tau_k$ as the *underlying path* of $\pi$. The *length* of the linear form is the length of the underlying path.

A linear form is described by the components above, where the exponents are given in binary. In the following, we show that every path can be transformed to a path in linear form with a small description size.

[lemma]{}[unaryLPF]{} \[lem:linear form of paths\] Let $\pi$ be an executable path of length $n$ from $(p,c)$ to $(q,c')$. Then there exists an executable path $\pi'$ of length $n$ in linear form whose length is at most $2|\states|^2$, from $(p,c)$ to $(q,c'')$ with $c''\ge c'$.

$\pi'$ is obtained from $\pi$ in two steps, namely rearranging simple cycles, and then choosing a small set of “representative” simple cycles to replace others. The crux of the proof is the first step, where instead of simply moving a cycle, we also shift it so that it is taken from its nadir. Then, for every set of simple cycles of the same length and on the same state, we take the one with maximal effect as a representative.

We now turn to identify states that have a 