GapCVP proof, part 04, continuation 04

noncomputable def GapCVP.OutputPolynomialCompositionClosure.markerConditionalComputable {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : BitTM (markerConditionalOutput valid fallback)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputPolynomialCompositionClosure.sourcePreservingConditionalComputable {selector : List Bool → Bool} {valid : List Bool → List Bool} (selection : BitTM fun (input : List Bool) => selector input :: input) (computer : BitTM valid) (fallback : List Bool) : BitTM fun (input : List Bool) => if selector input = true then valid input else fallback

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.CNFBoundedRecordFoldTM.actualWindowIndexEquiv (T : ℕ) : CL.Window T ≃ Fin T × CL.Position T

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalAtMostOneFamilyClauses (T S : ℕ) : List (CL.Clause T S)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalForbiddenTransitionFamilyClauses {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalFiveFamilySourceClauseCandidates {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CNFBoundedRecordFoldTM.totalFiveFamilySourceClauseCandidates_toFinset {T S : ℕ} (specification : CL.Specification T S) : (totalFiveFamilySourceClauseCandidates specification).toFinset = CL.tableauFormula specification

noncomputable def GapCVP.CNFBoundedRecordFoldTM.totalVerifierFiveFamilySourceClauseCandidates (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : List (CL.Clause (Polynomial.eval input.length (CLStructuralWholeCNFOutputTM.paddedStructuralTableauSimulation bound machine).time) (CLStructuralWholeCNFOutputTM.paddedStructuralTableauSimulation bound machine).symbols)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.CNFBoundedRecordFoldTM.totalVerifierFiveFamilySourceClauseCandidates_sorted (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : CNFFiniteRecordSort.sourceOrderedDistinctRecords (totalVerifierFiveFamilySourceClauseCandidates bound machine input) = CLStructuralWholeCNFOutputTM.structuralWholeSourceClauses bound machine input

theorem GapCVP.CNFBoundedRecordFoldTM.encodeThreeCNF_totalVerifierFiveFamilies (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : BinaryEncoding.encodeThreeCNF (ThreeCNFReduction.encodeFormulaFrom 0 (CNFFiniteRecordSort.sourceOrderedDistinctRecords (totalVerifierFiveFamilySourceClauseCandidates bound machine input))) = CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine input

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.CNFBoundedRecordFoldTM.polynomialValueUnaryComputable (polynomial : Polynomial ℕ) : BitTM fun (input : List Bool) => List.replicate (Polynomial.eval input.length polynomial) true

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

def GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold : List Bool → Option (ℕ × List Bool)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold [] = none
• GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold (false :: remaining) = some (0, remaining)

def GapCVP.OutputBoundedDependentRecordFold.unaryBoundedFoldWord (count : ℕ) (seed : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.OutputBoundedDependentRecordFold.unaryBoundedFoldWord count seed = List.replicate count true ++ false :: seed

@[simp]

theorem GapCVP.OutputBoundedDependentRecordFold.parseUnaryBoundedFold_word (count : ℕ) (seed : List Bool) : parseUnaryBoundedFold (unaryBoundedFoldWord count seed) = some (count, seed)

def GapCVP.OutputBoundedDependentRecordFold.boundedRecordFoldOutput (worker : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.OutputBoundedDependentRecordFold.parsedUnaryFold_count_le_length (input : List Bool) (count : ℕ) (seed : List Bool) (hparse : parseUnaryBoundedFold input = some (count, seed)) : count ≤ input.length

noncomputable def GapCVP.OutputBoundedDependentRecordFold.PolynomiallyBoundedFoldStates (worker : List Bool → List Bool) (bound : Polynomial ℕ) : Bool

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldMachine {worker : List Bool → List Bool} (computer : BitTM worker) : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) (configuration : computer.tm.Cfg) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerConfiguration_step {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) (configuration next : computer.tm.Cfg) (hstep : computer.tm.step configuration = some next) : (boundedDependentRecordFoldMachine computer).step (boundedFoldWorkerConfiguration computer counter configuration) = some (boundedFoldWorkerConfiguration computer counter next)

Internal support shared across GapCVP continuation modules.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldScanConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (remaining : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldDispatchConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldDrainConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (output : List (computer.tm.Γ computer.tm.k₁)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldRestoreConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GapCVP.OutputBoundedDependentRecordFold.boundedFoldMalformedConfiguration {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).Cfg

Internal support shared across GapCVP continuation modules.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFoldWorkerConfiguration_halt {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) (output : List (computer.tm.Γ computer.tm.k₁)) : boundedFoldWorkerConfiguration computer counter (Turing.haltList computer.tm output) = boundedFoldDrainConfiguration computer output counter []

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedDependentRecordFoldMachine_init {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) : Turing.initList (boundedDependentRecordFoldMachine computer) input = boundedFoldScanConfiguration computer input []

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_scan_true {worker : List Bool → List Bool} (computer : BitTM worker) (remaining : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer (computer.inputAlphabet.invFun true :: remaining) counter) = some (boundedFoldScanConfiguration computer remaining (true :: counter))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_scan_delimiter {worker : List Bool → List Bool} (computer : BitTM worker) (remaining : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer (computer.inputAlphabet.invFun false :: remaining) counter) = some (boundedFoldDispatchConfiguration computer remaining counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_scan_missing {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldScanConfiguration computer [] counter) = some (boundedFoldMalformedConfiguration computer counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_dispatch_step {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDispatchConfiguration computer input (true :: counter)) = some (boundedFoldWorkerConfiguration computer counter (Turing.initList computer.tm input))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_dispatch_finish {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDispatchConfiguration computer input []) = some (Turing.haltList (boundedDependentRecordFoldMachine computer) input)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_drain_step {worker : List Bool → List Bool} (computer : BitTM worker) (symbol : computer.tm.Γ computer.tm.k₁) (remaining : List (computer.tm.Γ computer.tm.k₁)) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDrainConfiguration computer (symbol :: remaining) counter scratch) = some (boundedFoldDrainConfiguration computer remaining counter (computer.outputAlphabet symbol :: scratch))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_drain_finish {worker : List Bool → List Bool} (computer : BitTM worker) (counter scratch : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldDrainConfiguration computer [] counter scratch) = some (boundedFoldRestoreConfiguration computer [] counter scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_restore_step {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) (bit : Bool) (scratch : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldRestoreConfiguration computer input counter (bit :: scratch)) = some (boundedFoldRestoreConfiguration computer (computer.inputAlphabet.invFun bit :: input) counter scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_restore_finish {worker : List Bool → List Bool} (computer : BitTM worker) (input : List (computer.tm.Γ computer.tm.k₀)) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldRestoreConfiguration computer input counter []) = some (boundedFoldDispatchConfiguration computer input counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_malformed_step {worker : List Bool → List Bool} (computer : BitTM worker) (counter : List Bool) : (boundedDependentRecordFoldMachine computer).step (boundedFoldMalformedConfiguration computer (true :: counter)) = some (boundedFoldMalformedConfiguration computer counter)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputBoundedDependentRecordFold.boundedFold_malformed_finish {worker : List Bool → List Bool} (computer : BitTM worker) : (boundedDependentRecordFoldMachine computer).step (boundedFoldMalformedConfiguration computer []) = some (Turing.haltList (boundedDependentRecordFoldMachine computer) [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFTypedRecordWorkerTM.parsedUnaryFold_seed_length_le (raw : List Bool) (count : ℕ) (seed : List Bool) (hparse : OutputBoundedDependentRecordFold.parseUnaryBoundedFold raw = some (count, seed)) : seed.length ≤ raw.length

theorem GapCVP.CNFTypedRecordWorkerTM.acceptanceClause_exact_card {T S : ℕ} (accept : CL.Symbol S) : Finset.card (CL.acceptanceClause accept) = T + 1