GapCVP proof, part 04, continuation 03

noncomputable def GapCVP.CLStructuralCNFOutputMachinesUnconditional.sourcePreservingPolynomialMarkerComputable (polynomial : Polynomial ℕ) : BitTM (CNFPolynomialRowMarkerTM.sourcePreservingPolynomialMarkerWord polynomial)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFDependentFiveFamilyRecordTM.executableAtLeastOneFamilyClauses (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.CNFDependentFiveFamilyRecordTM.executableAtMostOneFamilyClauses (T S : ℕ) : List (CL.Clause T S)

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFDependentFiveFamilyRecordTM.executableInitialFamilyClauses {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.

def GapCVP.CNFDependentFiveFamilyRecordTM.executableAcceptanceFamilyClauses {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

• GapCVP.CNFDependentFiveFamilyRecordTM.executableAcceptanceFamilyClauses specification = [GapCVP.CL.acceptanceClause specification.accept]

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

Internal support shared across GapCVP continuation modules.

Equations

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

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

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFDependentFiveFamilyRecordTM.executableFiveFamilySourceClauseCandidates_toFinset {T S : ℕ} (specification : CL.Specification T S) : (executableFiveFamilySourceClauseCandidates specification).toFinset = CL.tableauFormula specification

Internal support shared across GapCVP continuation modules.

def GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput (valid : List Bool → List Bool) (fallback : List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput valid fallback (true :: input) = valid input
• GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput valid fallback x✝ = fallback

@[reducible, inline]

abbrev GapCVP.OutputPolynomialCompositionClosure.ConditionalLabel (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.OutputPolynomialCompositionClosure.ConditionalLabel tm = (tm.Λ ⊕ Bool)

@[reducible, inline]

abbrev GapCVP.OutputPolynomialCompositionClosure.ConditionalState (tm : Turing.FinTM2) : Type

GapCVP reduction support.

Equations

• GapCVP.OutputPolynomialCompositionClosure.ConditionalState tm = (Option Bool × tm.σ)

@[reducible, inline]

abbrev GapCVP.OutputPolynomialCompositionClosure.liftValidStatement (tm : Turing.FinTM2) : Turing.TM2.Stmt (fun (k : tm.K) => tm.Γ (id k)) tm.Λ tm.σ → Turing.TM2.Stmt tm.Γ (tm.Λ ⊕ Bool) (Option Bool × tm.σ)

GapCVP reduction support.

Equations

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

@[reducible, inline]

noncomputable abbrev GapCVP.OutputPolynomialCompositionClosure.markerConditionalMachine {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : Turing.FinTM2

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.validConfiguration {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (configuration : computer.tm.Cfg) : (markerConditionalMachine computer fallback).Cfg

GapCVP reduction support.

Equations

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

theorem GapCVP.OutputPolynomialCompositionClosure.liftValidStatement_stepAux {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (statement : Turing.TM2.Stmt computer.tm.Γ computer.tm.Λ computer.tm.σ) (state : computer.tm.σ) (sourceStacks : (k : computer.tm.K) → List (computer.tm.Γ k)) : Turing.TM2.stepAux (liftValidStatement computer.tm statement) (some true, state) sourceStacks = validConfiguration computer fallback (Turing.TM2.stepAux statement state sourceStacks)

theorem GapCVP.OutputPolynomialCompositionClosure.validConfiguration_step {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (configuration next : computer.tm.Cfg) (hstep : computer.tm.step configuration = some next) : (markerConditionalMachine computer fallback).step (validConfiguration computer fallback configuration) = some (validConfiguration computer fallback next)

Internal support shared across GapCVP continuation modules.

@[simp]

theorem GapCVP.OutputPolynomialCompositionClosure.initialStack_input (tm : Turing.FinTM2) (input : List (tm.Γ tm.k₀)) : (Turing.initList tm input).stk tm.k₀ = input

@[simp]

theorem GapCVP.OutputPolynomialCompositionClosure.initialStack_empty (tm : Turing.FinTM2) (k : tm.K) : (Turing.initList tm []).stk k = []

noncomputable def GapCVP.OutputPolynomialCompositionClosure.fallbackConfiguration {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.OutputPolynomialCompositionClosure.fallbackTrace {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : StateTransition.EvalsToInTime (markerConditionalMachine computer fallback).step (fallbackConfiguration computer fallback remaining) (some (Turing.haltList (markerConditionalMachine computer fallback) (List.map computer.outputAlphabet.invFun fallback))) (remaining.length + 1)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.OutputPolynomialCompositionClosure.markerConditional_start_true {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (computer.inputAlphabet.invFun true :: remaining)) = some (validConfiguration computer fallback (Turing.initList computer.tm remaining))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputPolynomialCompositionClosure.markerConditional_start_false {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (remaining : List (computer.tm.Γ computer.tm.k₀)) : (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) (computer.inputAlphabet.invFun false :: remaining)) = some (fallbackConfiguration computer fallback remaining)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputPolynomialCompositionClosure.markerConditional_start_missing {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) : (markerConditionalMachine computer fallback).step (Turing.initList (markerConditionalMachine computer fallback) []) = some (fallbackConfiguration computer fallback [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.OutputPolynomialCompositionClosure.validConfiguration_halt {valid : List Bool → List Bool} (computer : BitTM valid) (fallback : List Bool) (output : List (computer.tm.Γ computer.tm.k₁)) : validConfiguration computer fallback (Turing.haltList computer.tm output) = Turing.haltList (markerConditionalMachine computer fallback) output

Internal support shared across GapCVP continuation modules.