GapCVP proof, part 07, continuation 02

noncomputable def GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFlatWholePackedInitialClauseRecordWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyFlatWholePackedInitialClauseRecordComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : BitTM (fiveFlatWholePackedInitialClauseRecordWord bound machine)

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.CNFFiveFamilyPackedInitialCellDecoderTM.fiveFamilyFlatWholePackedInitialClauseRecordWord_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (position : CL.Position (CLCellRowBounds.rowWidth bound machine original)) : fiveFlatWholePackedInitialClauseRecordWord bound machine (BinaryEncoding.lengthPrefixedWord (List.replicate (↑position) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (CL.initialClause (CLPaddedAcceptanceCompiler.paddedAcceptancePhaseSpecification bound machine original).input position)

inductive GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.FiveFamilyForbiddenWindowCoordinate : Type

GapCVP reduction support.

• left : FiveFamilyForbiddenWindowCoordinate
• center : FiveFamilyForbiddenWindowCoordinate
• right : FiveFamilyForbiddenWindowCoordinate
• next : FiveFamilyForbiddenWindowCoordinate

def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveForbiddenUnarySuccessorWord (source : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveForbiddenUnarySuccessorWord source input = true :: source input

noncomputable def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveForbiddenUnarySuccessorComputable {source : List Bool → List Bool} (computer : BitTM source) : BitTM (fiveForbiddenUnarySuccessorWord source)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveFamilyForbiddenWindowSourceRank {T : ℕ} (window : CL.Window T) : ℕ

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveForbiddenCoordinateSourceVariableCode (grid : Polynomial ℕ) (coordinate : FiveFamilyForbiddenWindowCoordinate) (symbol : ℕ) (input : List Bool) : List Bool

Internal support shared across GapCVP continuation modules.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveFamilyForbiddenCoordinateSourceVariableCodeComputable (grid : Polynomial ℕ) (coordinate : FiveFamilyForbiddenWindowCoordinate) (symbol : ℕ) : BitTM (fiveForbiddenCoordinateSourceVariableCode grid coordinate symbol)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveForbiddenWindowSourceVariable {T S : ℕ} (window : CL.Window T) (symbols : CL.WindowSymbols S) : FiveFamilyForbiddenWindowCoordinate → CL.Variable T S

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveFamilyForbiddenWindowSlotSymbol {S : ℕ} (symbols : CL.WindowSymbols S) : FiveFamilyForbiddenWindowCoordinate → CL.Symbol S

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveFamilyForbiddenWindowSlotSymbol symbols GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.FiveFamilyForbiddenWindowCoordinate.left = symbols.1

theorem GapCVP.CNFFiveFamilyForbiddenWindowCoordinateTM.fiveFamilyForbiddenCoordinateSourceVariableCode_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (window : CL.Window (CLCellRowBounds.rowWidth bound machine original)) (symbols : CL.WindowSymbols (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) (coordinate : FiveFamilyForbiddenWindowCoordinate) : fiveForbiddenCoordinateSourceVariableCode (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) coordinate (↑(fiveFamilyForbiddenWindowSlotSymbol symbols coordinate)) (BinaryEncoding.lengthPrefixedWord (List.replicate (fiveFamilyForbiddenWindowSourceRank window) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.replicate (Encodable.encode (fiveForbiddenWindowSourceVariable window symbols coordinate)) true