Lemma·L65
Parse balance is additive under concatenation
The balance after reading u then partway into v is u's ending balance, carried into v's own running balance.
For a language
,
, and
:
In words
For alphabet sequences u and v and j at most the length of v, the running 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 (D088) 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 D088: Since , (T29), so . By the induction hypothesis, . Substituting and regrouping (commutativity/associativity of ): the last step by the step clause of D088 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
The precise sense in which parse balance "picks up where it left off" across a concatenation: the
correction removes the extra unit that
counts as its own fresh starting debt, which is really a continuation of
's ending balance rather than a new one. Feeds directly into the balance invariant for terms, where a function application
is built by concatenating its argument terms one at a time, via associativity and the recursive characterization of n-ary concatenation.