GapCVP proof, part 06, continuation 04

noncomputable def GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionComputable : BitTM sourceUnaryDivisionOutput

GapCVP reduction support.

Equations

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

def GapCVP.SourceMixedRadixDimensionRowMajorIndexTM.sourceMixedRadixRowMajorPairOutput : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMixedRadixDimensionRowMajorIndexTM.sourceMixedRadixRowMajorPairOutput = GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionOutput

noncomputable def GapCVP.SourceMixedRadixDimensionRowMajorIndexTM.sourceMixedRadixRowMajorPairComputable : BitTM sourceMixedRadixRowMajorPairOutput

GapCVP reduction support.

Equations

• GapCVP.SourceMixedRadixDimensionRowMajorIndexTM.sourceMixedRadixRowMajorPairComputable = GapCVP.SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionComputable

@[simp]

theorem GapCVP.SourceMixedRadixDimensionRowMajorIndexTM.sourceMixedRadixRowMajorPairOutput_valid (rank dimension : ℕ) (source : List Bool) (hdimension : 0 < dimension) : sourceMixedRadixRowMajorPairOutput (SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionQuery rank dimension source) = List.replicate (rank / dimension) true ++ false :: (List.replicate (rank % dimension) true ++ false :: SourceMixedRadixUnaryQuotientRemainderTM.sourceUnaryDivisionQuery rank dimension source)

def GapCVP.SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixGuardedOriginalAtomOutput (atom : List Bool → List Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixGuardedOriginalAtomOutput atom = atom ∘ GapCVP.SourceFormulaStructuralDecoder.firstFieldContents

noncomputable def GapCVP.SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixGuardedOriginalAtomComputable {atom : List Bool → List Bool} (computer : BitTM atom) : BitTM (sourceMixedRadixGuardedOriginalAtomOutput atom)

GapCVP reduction support.

Equations

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

def GapCVP.SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixOriginalSourceQueryStream (queries : List (List Bool)) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceMixedRadixOriginalSourceDescriptorRotationTM.sourceMixedRadixOriginalSourceQueryStream queries = List.flatMap GapCVP.BinaryEncoding.lengthPrefixedWord queries

theorem GapCVP.SourceMixedRadixPolynomialPaddedDescriptorFoldTM.sourceMixedRadixPhysicalFirstFieldContents_length_le (input : List Bool) : (SourceFormulaStructuralDecoder.firstFieldContents input).length ≤ input.length

theorem GapCVP.SourceMixedRadixPolynomialPaddedDescriptorFoldTM.sourceMixedRadixPhysicalFirstFieldSuffix_length_le (input : List Bool) : (SourceFormulaStructuralDecoder.firstFieldSuffix input).length ≤ input.length

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseQuery (index : ℕ) (formula : ThreeCNF) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseQuery index formula = List.replicate index true ++ false :: GapCVP.BinaryEncoding.encodeThreeCNF formula

theorem GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedLiteralSuffix_length_le (input : List Bool) : (SourceFormulaStructuralDecoder.literalSuffix input).length ≤ input.length

theorem GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseSuffix_length_le (input : List Bool) : (SourceFormulaStructuralDecoder.clauseSuffix input).length ≤ input.length

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedLiteralSignOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedLiteralSignComputable : BitTM sourceOriginalIndexedLiteralSignOutput

GapCVP reduction support.

Equations

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

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedLiteralVariableOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedLiteralVariableOutput input = GapCVP.BinaryEncoding.lengthPrefixedWord (GapCVP.SourceFormulaStructuralDecoder.firstFieldContents input)

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedPhysicalLiteralOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedPhysicalLiteralComputable : BitTM sourceOriginalIndexedPhysicalLiteralOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedPhysicalLiteralOutput_valid (literal : Literal) (suffix : List Bool) : sourceOriginalIndexedPhysicalLiteralOutput (BinaryEncoding.encodeLiteral literal ++ suffix) = BinaryEncoding.encodeLiteral literal

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedSecondLiteralOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedThirdLiteralOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedPhysicalThreeClauseOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedPhysicalThreeClauseComputable : BitTM sourceOriginalIndexedPhysicalThreeClauseOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedPhysicalThreeClauseOutput_valid (clause : ThreeClause) (suffix : List Bool) : sourceOriginalIndexedPhysicalThreeClauseOutput (BinaryEncoding.encodeThreeClause clause ++ suffix) = BinaryEncoding.encodeThreeClause clause

def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseOutput : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseComputable : BitTM sourceOriginalIndexedClauseOutput

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceIndexedClauseLookupTM.sourceOriginalIndexedClauseOutput_valid (index : ℕ) (formula : ThreeCNF) (hindex : index < List.length formula) : sourceOriginalIndexedClauseOutput (sourceOriginalIndexedClauseQuery index formula) = BinaryEncoding.encodeThreeClause (List.get formula ⟨index, hindex⟩)

@[simp]

theorem GapCVP.SourceIndexedClauseSignTM.sourceOriginalIndexedLiteralSignOutput_valid (literal : Literal) (suffix : List Bool) : SourceIndexedClauseLookupTM.sourceOriginalIndexedLiteralSignOutput (BinaryEncoding.encodeLiteral literal ++ suffix) = [literal.2]

def GapCVP.SourceIndexedClauseSignTM.sourceOriginalClauseBooleanUnaryOutput : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceIndexedClauseSignTM.sourceOriginalClauseBooleanUnaryOutput = GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput (fun (x : List Bool) => [true]) []

noncomputable def GapCVP.SourceIndexedClauseSignTM.sourceOriginalClauseBooleanUnaryComputable : BitTM sourceOriginalClauseBooleanUnaryOutput

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceIndexedClauseSignTM.sourceOriginalClauseBooleanUnaryOutput_bit (sign : Bool) : sourceOriginalClauseBooleanUnaryOutput [sign] = List.replicate (if sign = true then 1 else 0) true

def GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRankSourcePair (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRawCandidate (candidate : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRawCandidate candidate input = candidate (GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRankSourcePair input)

def GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridCandidateSelector (candidate : List Bool → List Bool) (input : List Bool) : Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridCandidateSelector_eq (candidate : List Bool → List Bool) (input : List Bool) : sourceAnchoredGridCandidateSelector candidate input = decide ((sourceAnchoredGridRawCandidate candidate input).length ≤ (SourceFormulaStructuralDecoder.firstFieldContents input).length)

def GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridGuardedCandidate (candidate : 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.

def GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRecordRotationOutput (candidate : 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.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRecordRotationOutput_records (candidate : List Bool → List Bool) (anchor rank pending : List Bool) : sourceAnchoredGridRecordRotationOutput candidate (BinaryEncoding.lengthPrefixedWord anchor ++ BinaryEncoding.lengthPrefixedWord rank ++ pending) = BinaryEncoding.lengthPrefixedWord anchor ++ pending ++ BinaryEncoding.lengthPrefixedWord (sourceAnchoredGridGuardedCandidate candidate (BinaryEncoding.lengthPrefixedWord anchor ++ BinaryEncoding.lengthPrefixedWord rank ++ pending))

noncomputable def GapCVP.SourceAnchoredGridRecordFoldTM.sourceAnchoredGridRecordFoldComputable {candidate : List Bool → List Bool} (computer : BitTM candidate) : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput (sourceAnchoredGridRecordRotationOutput candidate))

GapCVP reduction support.

Equations

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

theorem GapCVP.SourceAnchoredGridRecordFoldTM.boundedRecordFoldOutput_sourceAnchoredGridRecordRanks (candidate : List Bool → List Bool) (anchor : List Bool) (ranks : List (List Bool)) (suffix : List Bool) (hfit : ∀ rank ∈ ranks, (candidate (BinaryEncoding.lengthPrefixedWord rank ++ anchor)).length ≤ anchor.length) : OutputBoundedDependentRecordFold.boundedRecordFoldOutput (sourceAnchoredGridRecordRotationOutput candidate) (OutputBoundedDependentRecordFold.unaryBoundedFoldWord ranks.length (BinaryEncoding.lengthPrefixedWord anchor ++ List.flatMap BinaryEncoding.lengthPrefixedWord ranks ++ suffix)) = BinaryEncoding.lengthPrefixedWord anchor ++ suffix ++ List.flatMap (fun (rank : List Bool) => BinaryEncoding.lengthPrefixedWord (candidate (BinaryEncoding.lengthPrefixedWord rank ++ anchor))) ranks

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedCatalogueTM.fiveFlatOriginalSourceAnchorWord (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.CNFFiveFamilyFlatIndexedCatalogueTM.fiveFamilyFlatOriginalSourceAnchorComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : BitTM (fiveFlatOriginalSourceAnchorWord bound machine)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedPhysicalRank (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedPhysicalRank input = GapCVP.SourceFormulaStructuralDecoder.firstFieldContents input

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedPhysicalRankComputable : BitTM fiveFamilyFlatIndexedPhysicalRank

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedPhysicalRankComputable = GapCVP.SourceFormulaStructuralDecoder.firstFieldContentsComputable

def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedPhysicalOriginal (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedPhysicalOriginalComputable : BitTM fiveFlatIndexedPhysicalOriginal

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedPhysicalRank_valid (rank : ℕ) (original suffix : List Bool) : fiveFamilyFlatIndexedPhysicalRank (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.replicate rank true

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedPhysicalOriginal_valid (rank : ℕ) (original suffix : List Bool) : fiveFlatIndexedPhysicalOriginal (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = original

def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedOriginalPolynomialUnary (polynomial : Polynomial ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedOriginalPolynomialUnaryComputable (polynomial : Polynomial ℕ) : BitTM (fiveFlatIndexedOriginalPolynomialUnary polynomial)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedOriginalPolynomialUnary_valid (polynomial : Polynomial ℕ) (rank : ℕ) (original suffix : List Bool) : fiveFlatIndexedOriginalPolynomialUnary polynomial (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.replicate (Polynomial.eval original.length polynomial) true

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : Polynomial ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine = GapCVP.CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine + 1

@[simp]

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial_eval (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : Polynomial.eval original.length (fiveFamilyFlatIndexedGridPolynomial bound machine) = CLCellRowBounds.rowWidth bound machine original + 1

def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedOriginalQuotientUnary (polynomial : Polynomial ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedOriginalQuotientUnaryComputable (polynomial : Polynomial ℕ) : BitTM (fiveFlatIndexedOriginalQuotientUnary polynomial)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFlatIndexedOriginalRemainderUnary (polynomial : Polynomial ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedOriginalRemainderUnaryComputable (polynomial : Polynomial ℕ) : BitTM (fiveFlatIndexedOriginalRemainderUnary polynomial)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedOriginalQuotientUnary_valid (polynomial : Polynomial ℕ) (rank : ℕ) (original suffix : List Bool) (hpositive : 0 < Polynomial.eval original.length polynomial) : fiveFlatIndexedOriginalQuotientUnary polynomial (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.replicate (rank / Polynomial.eval original.length polynomial) true

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedOriginalRemainderUnary_valid (polynomial : Polynomial ℕ) (rank : ℕ) (original suffix : List Bool) (hpositive : 0 < Polynomial.eval original.length polynomial) : fiveFlatIndexedOriginalRemainderUnary polynomial (BinaryEncoding.lengthPrefixedWord (List.replicate rank true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.replicate (rank % Polynomial.eval original.length polynomial) true

def GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedVariableCode (polynomial : Polynomial ℕ) (symbol : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridQuotient_lt (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : ℕ) (hrank : rank < (CLCellRowBounds.rowWidth bound machine original + 1) ^ 2) : rank / (CLCellRowBounds.rowWidth bound machine original + 1) < CLCellRowBounds.rowWidth bound machine original + 1

theorem GapCVP.CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridRemainder_lt (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) (rank : ℕ) : rank % (CLCellRowBounds.rowWidth bound machine original + 1) < CLCellRowBounds.rowWidth bound machine original + 1

def GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorTimePositionSlots (T : ℕ) : List (CL.Time T × CL.Position T)

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorTimePositionSlots T = GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorFinitePairs✝ (T + 1) (T + 1)

@[simp]

theorem GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.mem_fiveFamilyRowMajorTimePositionSlots {T : ℕ} (time : CL.Time T) (position : CL.Position T) : (time, position) ∈ fiveFamilyRowMajorTimePositionSlots T

def GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorSymbolPairs (S : ℕ) : List (CL.Symbol S × CL.Symbol S)

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorSymbolPairs S = GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorFinitePairs✝ (S + 1) (S + 1)

@[simp]

theorem GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorSymbolPairs_length (S : ℕ) : (fiveFamilyRowMajorSymbolPairs S).length = (S + 1) ^ 2

def GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorWindowSymbols (S : ℕ) : List (CL.WindowSymbols S)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorWindowSymbols_length (S : ℕ) : (fiveFamilyRowMajorWindowSymbols S).length = (S + 1) ^ 4

def GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorWindows (T : ℕ) : List (CL.Window T)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.mem_fiveFamilyRowMajorWindows {T : ℕ} (window : CL.Window T) : window ∈ fiveFamilyRowMajorWindows T

def GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorAtLeastClauses (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.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorAtMostClauses (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.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorInitialClauses {T S : ℕ} (specification : CL.Specification T S) : List (CL.Clause T S)

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorInitialClauses specification = List.map (GapCVP.CL.initialClause specification.input) (List.finRange (T + 1))

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

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorAcceptanceClauses specification = [GapCVP.CL.acceptanceClause specification.accept]

def GapCVP.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorForbiddenClauses {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.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorSourceClauses {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.CNFFiveFamilyFlatRowMajorCatalogueTM.fiveFamilyRowMajorSourceClauses_toFinset {T S : ℕ} (specification : CL.Specification T S) : (fiveFamilyRowMajorSourceClauses specification).toFinset = CL.tableauFormula specification

def GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalDynamicBitTail (index source : 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.

def GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalHeadBitWord : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalHeadBitWord = GapCVP.OutputPolynomialCompositionClosure.markerConditionalOutput (fun (x : List Bool) => [true]) [false]

noncomputable def GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalHeadBitComputable : BitTM fiveFamilyOriginalHeadBitWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalHeadBitWord_eq (input : List Bool) : fiveFamilyOriginalHeadBitWord input = [input.headD false]

def GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveFamilyOriginalDynamicBitWord (index source : 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.

noncomputable def GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveOriginalDynamicBitComputable {index source : List Bool → List Bool} (indexComputer : BitTM index) (sourceComputer : BitTM source) : BitTM (fiveFamilyOriginalDynamicBitWord index source)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyOriginalIndexedBitTM.fiveOriginalDynamicBitWord_valid (index source : List Bool → List Bool) (input : List Bool) (position : ℕ) (hindex : index input = List.replicate position true) : fiveFamilyOriginalDynamicBitWord index source input = [(List.drop position (source input)).headD false]

theorem GapCVP.CNFFiveFamilyFlatSortedLiteralFamilies.sortedElements_eq_of_nodup_source_pairwise {α : Type} [Encodable α] (records : Finset α) (candidate : List α) (hmembership : ∀ (record : α), record ∈ candidate ↔ record ∈ records) (hnodup : candidate.Nodup) (hpairwise : List.Pairwise (fun (first second : α) => Encodable.encode first ≤ Encodable.encode second) candidate) : ThreeCNFReduction.sortedElements records = candidate

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatRankedSourceDescriptorWord (grid : Polynomial ℕ) (symbol : ℕ) (sign : Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatRankedSourceDuplicatedCodeWord (grid : Polynomial ℕ) (symbol : ℕ) (sign : Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFlatRankedSourceDescriptorStream (grid : Polynomial ℕ) (sign : Bool) (symbols : List ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatRankedSourceDescriptorStreamComputable (grid : Polynomial ℕ) (sign : Bool) (symbols : List ℕ) : BitTM (fiveFlatRankedSourceDescriptorStream grid sign symbols)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFlatRankedSourceDuplicatedCodeStream (grid : Polynomial ℕ) (sign : Bool) (symbols : List ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatRankedSourceDuplicatedCodeStreamComputable (grid : Polynomial ℕ) (sign : Bool) (symbols : List ℕ) : BitTM (fiveFlatRankedSourceDuplicatedCodeStream grid sign symbols)

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFlatRowMajorAtLeastClauseRecordWord (grid : Polynomial ℕ) (alphabet : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatRowMajorAtLeastClauseRecordComputable (grid : Polynomial ℕ) (alphabet : ℕ) : BitTM (fiveFlatRowMajorAtLeastClauseRecordWord grid alphabet)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatSourceRowMajorIndex {T : ℕ} (time : CL.Time T) (position : CL.Position T) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatSourceRowMajorIndex time position = ↑time * (T + 1) + ↑position

@[simp]

theorem GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatSourceRowMajorIndex_div {T : ℕ} (time : CL.Time T) (position : CL.Position T) : fiveFamilyFlatSourceRowMajorIndex time position / (T + 1) = ↑time

@[simp]

theorem GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatSourceRowMajorIndex_mod {T : ℕ} (time : CL.Time T) (position : CL.Position T) : fiveFamilyFlatSourceRowMajorIndex time position % (T + 1) = ↑position

theorem GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFlatIndexedVariableCode_rowMajor (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (time : CL.Time (CLCellRowBounds.rowWidth bound machine original)) (position : CL.Position (CLCellRowBounds.rowWidth bound machine original)) (symbol : CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)) : CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedVariableCode (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) (↑symbol) (BinaryEncoding.lengthPrefixedWord (List.replicate (fiveFamilyFlatSourceRowMajorIndex time position) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = List.replicate (Encodable.encode (time, position, symbol)) true

theorem GapCVP.CNFFiveFamilyFlatRowMajorAtLeastClauseWorkerTM.fiveFamilyFlatRowMajorAtLeastClauseRecordWord_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original suffix : List Bool) (time : CL.Time (CLCellRowBounds.rowWidth bound machine original)) (position : CL.Position (CLCellRowBounds.rowWidth bound machine original)) : fiveFlatRowMajorAtLeastClauseRecordWord (CNFFiveFamilyFlatIndexedRankArithmeticTM.fiveFamilyFlatIndexedGridPolynomial bound machine) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm + 1) (BinaryEncoding.lengthPrefixedWord (List.replicate (fiveFamilyFlatSourceRowMajorIndex time position) true) ++ BinaryEncoding.lengthPrefixedWord original ++ suffix) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (CL.atLeastOneClause time position)

noncomputable def GapCVP.CNFFiveFamilyFlatAcceptanceVariableTM.fiveFamilyVerifierAcceptingSymbol {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : CL.Symbol (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyFlatAcceptanceClauseFoldTM.fiveFamilyFlatSingletonDescriptorPayload {T S : ℕ} (literal : CL.SignedLiteral T S) : CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseDescriptorPayload {literal} = CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (ThreeCNFReduction.sourceLiteral literal)

@[simp]

theorem GapCVP.CNFFiveFamilyFlatAcceptanceClauseFoldTM.fiveFamilyFlatSingletonDuplicatedCodePayload {T S : ℕ} (literal : CL.SignedLiteral T S) : CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseDuplicatedCodePayload {literal} = CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryField (Encodable.encode literal)

noncomputable def GapCVP.CNFFiveFamilyFlatAcceptanceClauseFoldTM.fiveFlatWholeAcceptanceClauseRecordWord (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFiveFamilyFlatAcceptanceClauseFoldTM.fiveFamilyFlatWholeAcceptanceClauseRecordComputable (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) : BitTM (fiveFlatWholeAcceptanceClauseRecordWord bound machine)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatAcceptanceClauseFoldTM.fiveFamilyFlatWholeAcceptanceClauseRecordWord_valid (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (original : List Bool) : fiveFlatWholeAcceptanceClauseRecordWord bound machine original = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord (CL.acceptanceClause (CNFFiveFamilyFlatAcceptanceVariableTM.fiveFamilyVerifierAcceptingSymbol machine))