The parse-balance invariant for formulas

Proof

1. 1
   Setup. By structural induction on : it suffices to prove the claim for every formula produced by each of the five clauses of D083 - equality, relation application, negation, a binary connective, or a quantifier - assuming it already holds of any formula(s) the clause is applied to.
2. 2
   Case eq. Let , , , , . By the step clause of D090 ( , so ): . Let . By L66 with , , : , using L67 applied to for . By L66 again with , , : , using L67 applied to . So .
3. 3
   Case eq, positivity. For : (base clause), so . For , write with : as in the Locality step of the proof of L66 (applicable since ), , and by L66 with : , using L67 (positivity, applied to ). For , write with : by L66 with : , using L67 (positivity, applied to ). Every falls in one of these ranges.
4. 4
   Case rel. Let with , with , . As in the proof of T31, for define , so and . Inner claim, every : Inner base : . , matching (relSym case of , D090). For ( ): .
5. 5
   Inner step ( ). Exactly as in the proof of T31 (via D080's recursive clause and associativity): . By L66 with , , : By the inner IH, the first term is ; by L67 applied to the term , the second is . Since (T29): . For positivity, let . If : Locality (as in L66's proof) gives by the inner IH. Otherwise for , and by L66: , using L67 (positivity, applied to ); as (naturals), by order-preservation of the embedding.
6. 6
   Case rel, conclude. T05 on gives the inner claim at , i.e. for : and for every . This is the theorem for this .
7. 7
   Case neg. Let already satisfy the theorem (inductive hypothesis, "IH"), , , . By the step clause of D090 ( for negation): . By L66 with , , : (IH, end). For : . For , write , : by L66, (IH, positivity). This is the theorem for this .
8. 8
   Case bin. Let , each already satisfy the theorem (IH), . Exactly as in case eq, with replaced by and L67 replaced by the IH on : (bin case of D090, matching the eq case's weight), so the identical two-step L66 argument (head then , then that combined with ) gives for , and the identical positivity argument (head region trivial via the base clause, then Locality plus L66 across each tail, using the IH's positivity on then on in place of L67) gives for every . This is the theorem for this .
9. 9
   Case quant. Let , , already satisfy the theorem (IH), , , . By two applications of the step clause of D090 ( for a quantifier, since matches none of 's funcSym, relSym, or logicSym cases): , then . Let , so and, by Locality (as in the proof of L66, since ), . By L66 with , , : (IH, end).
10. 10
    Case quant, positivity. For : . For : , shown above. For , write , : by L66 with : (IH, positivity). This is the theorem for this .
11. 11
    All five clauses of D083 preserve the theorem. By structural induction, the theorem holds for every .