Closure of FP under composition — proof internals

This module combines the sequential machine construction with polynomial normal forms for its two component computations. The public theorem is in Complexitylib.Classes.P.Composition.

theorem Complexity.mem_FP_comp_internal {f g : List Bool → List Bool} (hf : f ∈ FP) (hg : g ∈ FP) : g ∘ f ∈ FP

Internal proof that polynomial-time string functions are closed under function composition.