GapCVP proof, part 06

theorem GapCVP.CNFCappedFlatSourceListFoldTotalCert.flatUnaryDropFields_length_le (count : ℕ) (input : List Bool) : (CNFCappedFlatSourceListFoldTM.flatUnaryDropFields count input).length ≤ input.length

theorem GapCVP.CNFCappedFlatSourceListFoldTotalCert.sourcePairPrefixOutput_drop_length_le (pending : List Bool) : (CNFSourcePairPrefixWorkerTM.sourcePairPrefixOutput pending).length + (CNFCappedFlatSourceListFoldTM.flatUnaryDropFields 2 pending).length ≤ pending.length

def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.duplicatedUnarySignedLiteralCodeWord (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.CNFFiveFamilyFlatCandidateGenerationTM.duplicatedUnarySignedLiteralCodeComputable (sign : Bool) : BitTM (duplicatedUnarySignedLiteralCodeWord sign)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.duplicatedUnarySignedLiteralCodeWord_sourceVariable {T S : ℕ} (atom : CL.Variable T S) (sign : Bool) : duplicatedUnarySignedLiteralCodeWord sign (List.replicate (Encodable.encode atom) true) = CNFCappedFlatSourceListFoldTM.flatDuplicatedUnaryField (Encodable.encode (atom, sign))

def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseDescriptorPayload {T S : ℕ} (clause : CL.Clause T S) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseDuplicatedCodePayload {T S : ℕ} (clause : CL.Clause T S) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseUnaryCountPayload {T S : ℕ} (clause : CL.Clause T S) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseUnaryCountPayload clause = List.replicate (Finset.card clause) true

def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord {T S : ℕ} (clause : CL.Clause T S) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseUnaryCountPayload_length {T S : ℕ} (clause : CL.Clause T S) : (flatSourceClauseUnaryCountPayload clause).length = (CNFFlatSourceOrder.flatSourceFinsetCodes clause).length

def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceAnnotatedClauseLengthBound (T S : ℕ) : ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord_length_le {T S : ℕ} (clause : CL.Clause T S) : (flatSourceClauseAnnotatedRecord clause).length ≤ flatSourceAnnotatedClauseLengthBound T S

noncomputable def GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceAnnotatedClauseLengthPolynomial (time : Polynomial ℕ) (symbols : ℕ) : Polynomial ℕ

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFFiveFamilyFlatCandidateGenerationTM.flatSourceAnnotatedClauseLengthBound_eq_polynomial (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : flatSourceAnnotatedClauseLengthBound (CLCellRowBounds.rowWidth bound machine input) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm) = Polynomial.eval input.length (flatSourceAnnotatedClauseLengthPolynomial (CLNondeterminism.nondeterministicTableauDimensionPolynomial bound machine) (CLCompleteVerifierSimulation.completePhaseSymbolCount machine.tm))

def GapCVP.CNFCappedFlatSourceListComparatorTM.fullCappedFlatSourceListBinaryWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFCappedFlatSourceListComparatorTM.fullCappedFlatSourceListBinaryComputable : BitTM fullCappedFlatSourceListBinaryWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFCappedFlatSourceListComparatorTM.fullCappedFlatSourceListBinaryWord_valid (cap : ℕ) (records : List ℕ) : fullCappedFlatSourceListBinaryWord (OutputBoundedDependentRecordFold.unaryBoundedFoldWord records.length (CNFCappedFlatSourceListFoldTM.flatCappedUnarySourceListState cap 0 records.reverse)) = Computability.encodeNat (CNFFlatSourceOrder.cappedFlatSourceListValue cap records)

noncomputable def GapCVP.SourceCanonicalFixedWordTuringTM.sourceFixedWordComputable (word : List Bool) : BitTM fun (x : List Bool) => word

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldTail (offset : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldTail offset input = GapCVP.SourceFormulaStructuralDecoder.firstFieldSuffix^[offset] input

noncomputable def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceFieldTailComputable (offset : ℕ) : BitTM (flatAnnotatedSourceFieldTail offset)

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceFieldTailComputable 0 = id (Turing.idComputableInPolyTime GapCVP.bitEncoding)

def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt (offset : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceFieldAtComputable (offset : ℕ) : BitTM (flatAnnotatedSourceFieldAt offset)

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.annotatedSourceAdjacentClauseWord (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt_firstCodes (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) : flatAnnotatedSourceFieldAt 1 (annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix) = firstCodes

@[simp]

theorem GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt_firstCount (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) : flatAnnotatedSourceFieldAt 2 (annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix) = List.replicate firstCount true

@[simp]

theorem GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt_secondCodes (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) : flatAnnotatedSourceFieldAt 4 (annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix) = secondCodes

@[simp]

theorem GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceFieldAt_secondCount (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) : flatAnnotatedSourceFieldAt 5 (annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix) = List.replicate secondCount true

def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceZipCountWord (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceZipCountWord input = (GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceMinimumCountWord✝ input).tail

noncomputable def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceZipCountComputable : BitTM flatAnnotatedSourceZipCountWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourceZipCountWord_valid (firstClause firstCodes : List Bool) (firstCount : ℕ) (secondClause secondCodes : List Bool) (secondCount : ℕ) (suffix : List Bool) : flatAnnotatedSourceZipCountWord (annotatedSourceAdjacentClauseWord firstClause firstCodes firstCount secondClause secondCodes secondCount suffix) = List.replicate (min firstCount secondCount - 1) true

def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.flatAnnotatedSourcePrefixedField (offset : ℕ) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFAnnotatedSourceClausePairPreparationTM.annotatedSourcePrefixedFieldComputable (offset : ℕ) : BitTM (flatAnnotatedSourcePrefixedField offset)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatAdjacentConditionalSwapTM.flatAdjacentConditionalSwapOutput : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFlatAdjacentConditionalSwapTM.flatAdjacentConditionalSwapOutput (true :: input) = GapCVP.CNFFlatAdjacentRecordSwapTM.flatAdjacentRecordSwapOutput input
• GapCVP.CNFFlatAdjacentConditionalSwapTM.flatAdjacentConditionalSwapOutput (false :: input) = input
• GapCVP.CNFFlatAdjacentConditionalSwapTM.flatAdjacentConditionalSwapOutput [] = []

noncomputable def GapCVP.CNFFlatAdjacentConditionalSwapTM.flatAdjacentConditionalSwapComputable : BitTM flatAdjacentConditionalSwapOutput

GapCVP reduction support.

Equations

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

def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.keepFirstDropSecondWord : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFGuardedFiveFamilyTagDispatchTM.keepFirstDropSecondWord [] = []
• GapCVP.CNFGuardedFiveFamilyTagDispatchTM.keepFirstDropSecondWord (bit :: remaining) = bit :: remaining.tail

noncomputable def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.keepFirstDropSecondComputable : BitTM keepFirstDropSecondWord

GapCVP reduction support.

Equations

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

def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.encodedOrderingEqualityBitWord : List Bool → List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.encodedOrderingEqualityBitComputable : BitTM encodedOrderingEqualityBitWord

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFGuardedFiveFamilyTagDispatchTM.encodedOrderingEqualityBitWord_ordering (outcome : CNFEncodedClauseSort.EncodedWordOrdering) : encodedOrderingEqualityBitWord (CNFEncodedClauseSort.encodedWordOrderingWord outcome) = [decide (outcome = CNFEncodedClauseSort.EncodedWordOrdering.equal)]

def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedWordEqualityBitWord (expected input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedWordEqualityBitComputable (expected : List Bool) : BitTM (fixedDelimitedWordEqualityBitWord expected)

GapCVP reduction support.

Equations

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

def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedWordEqualitySelector (expected input : List Bool) : Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedWordEqualityBitWord_eq (expected input : List Bool) : fixedDelimitedWordEqualityBitWord expected input = [fixedDelimitedWordEqualitySelector expected input]

@[simp]

theorem GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedWordEqualitySelector_valid (expected actual suffix : List Bool) : fixedDelimitedWordEqualitySelector expected (BinaryEncoding.lengthPrefixedWord actual ++ suffix) = decide (expected = actual)

def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedGuardedWorkerWord (expected : List Bool) (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.

noncomputable def GapCVP.CNFGuardedFiveFamilyTagDispatchTM.fixedDelimitedGuardedWorkerComputable (expected : List Bool) {worker : List Bool → List Bool} (computer : BitTM worker) : BitTM (fixedDelimitedGuardedWorkerWord expected worker)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatCappedComparisonControlledSwapTM.flatComparisonGreaterMarker (comparison : List Bool → List Bool) (input : List Bool) : Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseRecord {T S : ℕ} (clause : CL.Clause T S) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseStream {T S : ℕ} (clauses : List (CL.Clause T S)) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseStream clauses = List.flatMap GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledClauseRecord clauses

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.annotatedBundledPairComparisonInput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.annotatedBundledPairComparisonWord (comparison : List Bool → List Bool) (input : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFAnnotatedSourceClauseBubblePassTM.annotatedBundledPairComparisonWord comparison input = comparison (GapCVP.CNFAnnotatedSourceClauseBubblePassTM.annotatedBundledPairComparisonInput input)

noncomputable def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledPairComparisonComputable {comparison : List Bool → List Bool} (computer : BitTM comparison) : BitTM (annotatedBundledPairComparisonWord comparison)

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBundledPairComparisonInput_records {T S : ℕ} (first second : CL.Clause T S) (suffix : List Bool) : annotatedBundledPairComparisonInput (flatAnnotatedBundledClauseRecord first ++ flatAnnotatedBundledClauseRecord second ++ suffix) = CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord first ++ CNFFiveFamilyFlatCandidateGenerationTM.flatSourceClauseAnnotatedRecord second

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubblePassState (active emitted : List Bool) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubblePassState active emitted = GapCVP.BinaryEncoding.lengthPrefixedWord active ++ GapCVP.BinaryEncoding.lengthPrefixedWord emitted

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubblePassStep (comparison : 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.CNFAnnotatedSourceClauseBubblePassTM.annotatedStructuralFieldAccounting (input : List Bool) : 2 * (SourceFormulaStructuralDecoder.firstFieldContents input).length + (SourceFormulaStructuralDecoder.firstFieldSuffix input).length ≤ input.length

theorem GapCVP.CNFAnnotatedSourceClauseBubblePassTM.annotatedStructuralTwoFieldAccounting (input : List Bool) : 2 * (SourceFormulaStructuralDecoder.firstFieldContents input).length + 2 * (SourceFormulaStructuralDecoder.firstFieldContents (SourceFormulaStructuralDecoder.firstFieldSuffix input)).length ≤ input.length

theorem GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubblePassStep_iterate_length_le (comparison : List Bool → List Bool) (input : List Bool) (count : ℕ) : ((flatAnnotatedBubblePassStep comparison)^[count] input).length ≤ input.length + 4 * count

noncomputable def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubblePassFoldComputable {comparison : List Bool → List Bool} (computer : BitTM comparison) : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput (flatAnnotatedBubblePassStep comparison))

GapCVP reduction support.

Equations

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

def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubbleClauseState {T S : ℕ} (active emitted : List (CL.Clause T S)) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFAnnotatedSourceClauseBubblePassTM.CorrectFlatAnnotatedBundledSourceComparison (comparison : List Bool → List Bool) : Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFAnnotatedSourceClauseBubblePassTM.flatAnnotatedBubblePassStep_clauseState {comparison : List Bool → List Bool} (hcomparison : CorrectFlatAnnotatedBundledSourceComparison comparison = true) {T S : ℕ} (first second : CL.Clause T S) (remaining emitted : List (CL.Clause T S)) : flatAnnotatedBubblePassStep comparison (flatAnnotatedBubbleClauseState (first :: second :: remaining) emitted) = if Encodable.encode second < Encodable.encode first then flatAnnotatedBubbleClauseState (first :: remaining) (emitted ++ [second]) else flatAnnotatedBubbleClauseState (second :: remaining) (emitted ++ [first])

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationQuery (left right : ℕ) : List Bool

GapCVP reduction support.

Equations

• GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationQuery left right = List.replicate left true ++ false :: List.replicate right true

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationOutput_query (left right : ℕ) : sourceUnaryIntegerMultiplicationOutput (sourceUnaryIntegerMultiplicationQuery left right) = List.replicate (left * right) true

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationLeftStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationRightStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationOuterStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationCopyStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationSuccessCleanupStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationFailureInputStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationFailureLeftStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationFailureRightStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationFailureRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationFailureOutputStatement : Turing.TM2.Stmt (fun (x : Fin 5) => Bool) (Fin 11) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

@[reducible, inline]

abbrev GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplicationConfiguration (phase : Fin 11) (input left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

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

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceUnaryIntegerMultiplicationMachine_init (input : List Bool) : Turing.initList sourceUnaryIntegerMultiplicationMachine input = sourceIntegerMultiplicationConfiguration 0 input [] [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.SourceUnaryIntegerMultiplicationTM.tacticSourceIntegerMultiplicationStepTac : Lean.ParserDescr

Executes the sourceIntegerMultiplicationStepTac machine-step simplifier.

Equations

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

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_left_true (input left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 0 (true :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 0 input (true :: left) right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_left_delimiter (input left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 0 (false :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 1 input left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_left_missing (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 0 [] left right restore output) = some (sourceIntegerMultiplicationConfiguration 6 [] left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_right_true (input left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 1 (true :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 1 input left (true :: right) restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_right_false (input left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 1 (false :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 6 input left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_right_finish (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 1 [] left right restore output) = some (sourceIntegerMultiplicationConfiguration 2 [] left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_outer_step (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 2 [] (true :: left) right restore output) = some (sourceIntegerMultiplicationConfiguration 3 [] left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_outer_finish (right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 2 [] [] right restore output) = some (sourceIntegerMultiplicationConfiguration 5 [] [] right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_copy_step (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 3 [] left (true :: right) restore output) = some (sourceIntegerMultiplicationConfiguration 3 [] left right (true :: restore) (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_copy_finish (left restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 3 [] left [] restore output) = some (sourceIntegerMultiplicationConfiguration 4 [] left [] restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_restore_step (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 4 [] left right (true :: restore) output) = some (sourceIntegerMultiplicationConfiguration 4 [] left (true :: right) restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_restore_finish (left right output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 4 [] left right [] output) = some (sourceIntegerMultiplicationConfiguration 2 [] left right [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_success_step (right output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 5 [] [] (true :: right) [] output) = some (sourceIntegerMultiplicationConfiguration 5 [] [] right [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_success_finish (output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 5 [] [] [] [] output) = some (Turing.haltList sourceUnaryIntegerMultiplicationMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_input_step (bit : Bool) (input left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 6 (bit :: input) left right restore output) = some (sourceIntegerMultiplicationConfiguration 6 input left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_input_finish (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 6 [] left right restore output) = some (sourceIntegerMultiplicationConfiguration 7 [] left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_left_step (bit : Bool) (left right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 7 [] (bit :: left) right restore output) = some (sourceIntegerMultiplicationConfiguration 7 [] left right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_left_finish (right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 7 [] [] right restore output) = some (sourceIntegerMultiplicationConfiguration 8 [] [] right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_right_step (bit : Bool) (right restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 8 [] [] (bit :: right) restore output) = some (sourceIntegerMultiplicationConfiguration 8 [] [] right restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_right_finish (restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 8 [] [] [] restore output) = some (sourceIntegerMultiplicationConfiguration 9 [] [] [] restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_restore_step (bit : Bool) (restore output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 9 [] [] [] (bit :: restore) output) = some (sourceIntegerMultiplicationConfiguration 9 [] [] [] restore output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_restore_finish (output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 9 [] [] [] [] output) = some (sourceIntegerMultiplicationConfiguration 10 [] [] [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_output_step (bit : Bool) (output : List Bool) : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 10 [] [] [] [] (bit :: output)) = some (sourceIntegerMultiplicationConfiguration 10 [] [] [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.SourceUnaryIntegerMultiplicationTM.sourceIntegerMultiplication_failure_finish : sourceUnaryIntegerMultiplicationMachine.step (sourceIntegerMultiplicationConfiguration 10 [] [] [] [] []) = some (Turing.haltList sourceUnaryIntegerMultiplicationMachine [])

Internal support shared across GapCVP continuation modules.