 Indexed beta reduction

Use the binary finite-set encoding $e_k$ and Cantor code $⟨k,t⟩$. Contracting $(\lambda x.P^n{)}^{m+1}{Q}^p$ gives the substituted body with its root index lowered by taking the minimum with $\min (m,n)$, replacing each occurrence $x^r$ by a copy of $Q$ with root index $\min (m,p,r)$. A zero-indexed abstraction instead substitutes $\perp$ and gives the body root index zero. Indices strictly budget the argument information that can be used by application. Finite-witness inequalities for the pairing code prove that indexed reduction increases the interpretation, although it can decrease the underlying Böhm tree.