Sequential composition correctness — proof internals #
This module connects the first function computation's placed raw-output boundary to the normalization tail. It derives coarse monotone time bounds for both function composition and preprocessing followed by a language decider.
theorem
Complexity.TM.compositionTM_computesInTime_internal
{nf ng : ℕ}
{tmF : TM nf}
{tmG : TM ng}
{f g : List Bool → List Bool}
{TF TG : ℕ → ℕ}
(hF : tmF.ComputesInTime f TF)
(hG : tmG.ComputesInTime g TG)
(hmono : Monotone TG)
:
(tmF.compositionTM tmG).ComputesInTime (g ∘ f) fun (n : ℕ) => 4 * TF n + 11 + TG (TF n)
Internal correctness theorem for the executable sequential function composition machine.
theorem
Complexity.TM.compositionTM_decidesInTime_preimage_internal
{nf ng : ℕ}
{tmF : TM nf}
{tmG : TM ng}
{f : List Bool → List Bool}
{L : Language}
{TF TG : ℕ → ℕ}
(hF : tmF.ComputesInTime f TF)
(hG : tmG.DecidesInTime L TG)
(hmono : Monotone TG)
:
(tmF.compositionTM tmG).DecidesInTime (f ⁻¹' L) fun (n : ℕ) => 4 * TF n + 11 + TG (TF n)
Internal correctness theorem for deterministic preprocessing followed by a language decider.