Theorem·T31
The parse-balance invariant for terms
Every term drives its own parse balance down to exactly zero, and never earlier: the running balance stays positive until the very last symbol.
For a language
and
with
:
and
In words
For any term of the language, with n its length as a symbol sequence: its parse balance reaches exactly zero after reading all n symbols, and it never reaches down to zero earlier - the running balance stays at least one at every position before the last.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1Setup. We argue by structural induction on : it suffices to prove the claim for every , and to show it is preserved by whenever it already holds of every entry of .
- 2Base case. Let , so . By the base clause, , giving the "pos" claim at the only , namely (as ). For "end": , which is never of the form for any , since in ((P3) applied twice: , hence by symmetry) and the characteristic property of ordered pairs would force if the tags matched. So (the "otherwise" branch), and .
- 3Step case, setup. Let with , and with , such that every entry ( ) already satisfies the theorem (inductive hypothesis, "IH"). Write . For define , so (the base clause gives , and concatenating with changes nothing, D075) and (as ). Inner claim, for every :
- 4Inner base, . . , matching . For (only ): .
- 5Inner step, ( ), the value. By the step clause of D080 applied to (length ), . So, using associativity of : By L65 with , , : By the inner IH at , the first term is ; by the outer IH applied to the term , the second is . And (T29). So
- 6Inner step, positivity. Let . If : the same locality argument as in the proof of L65 gives , which is by the inner IH. Otherwise for some , and by L65 (applicable since ): ; since , the outer IH gives , so . As (naturals), once embedded in (order-preservation of the embedding), so either way.
- 7Conclude. T05 on gives the inner claim at , i.e. for : and for every . This is exactly the outer theorem for , completing the step case. By structural induction, the theorem holds for every .
∎
Remarks
The technical heart of unique readability: it says a term never "finishes early" (no proper prefix is itself already balanced) and finishes exactly on time. Combined with the definition, this is what makes the actual uniqueness of a term's decomposition provable, which in turn is what will let a value or a satisfaction clause be assigned to a term or formula by genuine structural recursion rather than an unjustified leap. The double induction here - structural on the term, numerical on the number of arguments already processed within a function application - is the standard shape of this argument in every rigorous treatment of first-order syntax.