Lemma·L66
Formula parse balance is additive under concatenation
The same additivity property as for term balance, restated for the extended formula weight function.
For a language
,
, and
:
In words
For alphabet sequences u and v and j at most the length of v, the running formula balance after reading all of u and then j symbols into v equals u's own final balance, combined with v's balance after j symbols, minus the double-counted starting debt of one.
Never needed: F05 · F10 · F13 · A03 · A04 · A05 (computed from the citation graph, not asserted).
Proof
- 1Locality. For : . By induction on : at both equal (base clause). Suppose for some . Since (T29, as ), the case splits defining and (D090) test the same value, so , and the step clauses give . This holds for every .
- 2Base . (D027), so by Locality . And , so the claimed right side is : both sides agree.
- 3Step. Let and assume the claim at . Then (D027), so by the step clause of D090: Since , (T29), so . By the induction hypothesis, . Substituting and regrouping (commutativity/associativity of ): the last step by the step clause of D090 for : this matches the claim at .
- 4Let (Separation). Step 2 gives . If and , then (L15 (vi), transitivity), so and ; membership gives the claim at , and Step 3 upgrades it to : so . T05 gives , i.e. the claim holds for every .
∎
Remarks
Identical in every step to the term version, with
and
replaced throughout by "fbal" and h; nothing in the argument used any property of
beyond its being some fixed function of the symbol at each position, and
has exactly that shape. Feeds into the balance invariant for formulas the same way L65 feeds into T31.