Proof of `Regular terms define regular functions`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Every function defined by a regular term is regular under string representation (Theorem C.5.4, the implication from terms to regular functions): induction on the term, every atomic term being computed on representations by a rational or regular function that parses the representation with a capped bracket counter, and the combinators preserving regularity under representation ().
Proof strategy
The concept's terms are moved to the source's by , the elements of a type along , and the semantics commute (), so the transported function is defined by a source term (). The source theorem makes it regular under the source's representation, and brings it back: the representations agree up to the renaming of the alphabets (), and a regular function conjugated by that renaming is regular, through Part C §1–3's bridge for the regular functions.
Attribution
Theorem C.5.4 of Transducers, Part C; formalised by Aristotle (Harmonic), .