GapCVP proof, part 04, continuation 06

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPrefixTrace (sign : Option Bool) (count : ℕ) (tail counter reversed markers suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign (List.replicate count true ++ false :: tail) counter reversed markers suffix output) (some (flatLiteralRecordConfiguration 1 sign tail (List.replicate count true ++ counter) reversed markers suffix output)) (count + 1)

Scans a length prefix through its delimiter and enters the sign-reading phase.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordMissingPrefixTrace (sign : Option Bool) (count : ℕ) (counter reversed markers suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 sign (List.replicate count true) counter reversed markers suffix output) (some (flatLiteralRecordConfiguration 7 sign [] (List.replicate count true ++ counter) reversed markers suffix output)) (count + 1)

Sends an unterminated length prefix to invalid-input handling.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordPayloadTrace (sign : Bool) (payload input reversed markers suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 (some sign) (payload ++ input) (List.replicate payload.length true) reversed markers suffix output) (some (flatLiteralRecordConfiguration 3 (some sign) input [] (payload.reverse ++ reversed) (List.replicate payload.length true ++ markers) suffix (sign :: output))) (payload.length + 1)

Copies a complete literal payload into the reversed and marker stacks.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordRestoreTrace (sign : Option Bool) (input reversed markers suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 3 sign input [] reversed markers suffix output) (some (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix (false :: (reversed.reverse ++ output)))) (reversed.length + 1)

Restores the payload bits to the output after reading a literal.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordMarkerTrace (sign : Option Bool) (input markers suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 4 sign input [] [] markers suffix output) (some (flatLiteralRecordConfiguration 5 sign input [] [] [] suffix (List.replicate markers.length true ++ output))) (markers.length + 1)

Moves payload length markers to the output as a unary prefix.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSuffixScanTrace (sign : Option Bool) (input suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 5 sign input [] [] [] suffix output) (some (flatLiteralRecordConfiguration 6 sign [] [] [] [] (input.reverse ++ suffix) output)) (input.length + 1)

Moves the unread suffix to the scratch stack before finishing output.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordSuffixRestoreTrace (sign : Option Bool) (suffix output : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 6 sign [] [] [] [] suffix output) (some (Turing.haltList actualFlatLiteralRecordWorker (suffix.reverse ++ output))) (suffix.length + 1)

Restores the suffix from scratch and halts with the completed output.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordInvalidTrace (sign : Option Bool) (input count reversed markers : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 7 sign input count reversed markers [] []) (some (Turing.haltList actualFlatLiteralRecordWorker [])) (input.length + count.length + reversed.length + markers.length + 1)

Clears every occupied stack of an invalid literal record and halts empty.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordTruncatedPayloadTrace (sign : Bool) (payload : List Bool) (count : ℕ) (hshort : payload.length < count) (reversed markers : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 2 (some sign) payload (List.replicate count true) reversed markers [] []) (some (flatLiteralRecordConfiguration 7 (some sign) [] (List.replicate (count - payload.length) true) (payload.reverse ++ reversed) (List.replicate payload.length true ++ markers) [] [])) (payload.length + 1)

Detects a payload shorter than its length prefix and enters invalid-input handling.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordValidTrace (sign : Bool) (payload suffix : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 none (BinaryEncoding.lengthPrefixedWord (sign :: payload) ++ suffix) [] [] [] [] []) (some (Turing.haltList actualFlatLiteralRecordWorker (suffix ++ BinaryEncoding.lengthPrefixedWord payload ++ [sign]))) (8 * (BinaryEncoding.lengthPrefixedWord (sign :: payload) ++ suffix).length + 16)

Converts a valid length-prefixed signed literal to its flat record encoding.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatLiteralRecordTotalTrace (input : List Bool) : StateTransition.EvalsToInTime actualFlatLiteralRecordWorker.step (flatLiteralRecordConfiguration 0 none input [] [] [] [] []) (some (Turing.haltList actualFlatLiteralRecordWorker (flatLiteralRecordStep input))) (20 * input.length + 30)

Runs the literal-record worker on every input within a linear step bound.

Equations

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

noncomputable def GapCVP.CNFFlatStructuralRecordWorkerTM.actualFlatLiteralRecordWorkerComputable : BitTM flatLiteralRecordStep

Polynomial-time machine computing one flat literal-record step.

Equations

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

noncomputable def GapCVP.CNFFlatStructuralRecordWorkerTM.actualFlatLiteralRecordFoldComputable : BitTM (OutputBoundedDependentRecordFold.boundedRecordFoldOutput flatLiteralRecordStep)

Polynomial-time machine repeatedly applying the flat literal-record step.

Equations

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

def GapCVP.CNFFlatStructuralRecordWorkerTM.flatThreeClauseLiterals (clauses : ThreeCNF) : List Literal

GapCVP reduction support.

Equations

• GapCVP.CNFFlatStructuralRecordWorkerTM.flatThreeClauseLiterals clauses = List.flatMap (fun (clause : GapCVP.ThreeClause) => [clause 0, clause 1, clause 2]) clauses

def GapCVP.CNFFlatSourceOrder.cappedFlatSourceListValue (cap : ℕ) : List ℕ → ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceOrder.cappedFlatSourceListValue cap [] = 0
• GapCVP.CNFFlatSourceOrder.cappedFlatSourceListValue cap (head :: tail) = min cap (Nat.pair head (GapCVP.CNFFlatSourceOrder.cappedFlatSourceListValue cap tail)).succ

def GapCVP.CNFFlatSourceOrder.flatSourceNaturalOrdering (first second : ℕ) : CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatSourceOrder.resolveFlatSourceOrder (major : CNFEncodedClauseSort.EncodedWordOrdering) (first second : ℕ) : CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceOrder.resolveFlatSourceOrder GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal first second = GapCVP.CNFFlatSourceOrder.flatSourceNaturalOrdering first second
• GapCVP.CNFFlatSourceOrder.resolveFlatSourceOrder major first second = major

@[irreducible]

def GapCVP.CNFFlatSourceOrder.flatSortedSourceListOrdering : List ℕ → List ℕ → CNFEncodedClauseSort.EncodedWordOrdering

GapCVP reduction support.

Equations

• One or more equations did not get rendered due to their size.
• GapCVP.CNFFlatSourceOrder.flatSortedSourceListOrdering [] [] = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.equal
• GapCVP.CNFFlatSourceOrder.flatSortedSourceListOrdering [] (head :: tail) = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.less
• GapCVP.CNFFlatSourceOrder.flatSortedSourceListOrdering (head :: tail) [] = GapCVP.CNFEncodedClauseSort.EncodedWordOrdering.greater

def GapCVP.CNFFlatSourceOrder.flatSourceFinsetCodes {α : Type} [Encodable α] (records : Finset α) : List ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceOrder.flatSourceFinsetCodes records = List.map Encodable.encode (GapCVP.ThreeCNFReduction.sortedElements records)

theorem GapCVP.CNFFlatSourceOrder.flatSourceFinsetOrdering_eq_godel {α : Type} [Encodable α] (first second : Finset α) : flatSortedSourceListOrdering (flatSourceFinsetCodes first) (flatSourceFinsetCodes second) = flatSourceNaturalOrdering (Encodable.encode first) (Encodable.encode second)

theorem GapCVP.CNFFlatSourceOrder.flatSourceFinsetOrdering_equal_iff {α : Type} [Encodable α] (first second : Finset α) : flatSortedSourceListOrdering (flatSourceFinsetCodes first) (flatSourceFinsetCodes second) = CNFEncodedClauseSort.EncodedWordOrdering.equal ↔ first = second

def GapCVP.CNFFlatWholeWordFoldTM.structuralThreeCNFFlatFoldInput (clauses : ThreeCNF) : List Bool

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFFlatWholeWordFoldTM.totalVerifierSortedFiveFamilyFlatFoldInput (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.

theorem GapCVP.CNFFlatWholeWordFoldTM.boundedRecordFoldOutputTotalVerifierSortedFiveFamilies (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (input : List Bool) : OutputBoundedDependentRecordFold.boundedRecordFoldOutput CNFFlatStructuralRecordWorkerTM.flatLiteralRecordStep (totalVerifierSortedFiveFamilyFlatFoldInput bound machine input) = CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine input

noncomputable def GapCVP.CNFFlatWholeWordFoldTM.actualWholeStructuralCNFOutputComputableOfFlatPreparation (bound : Polynomial ℕ) {verifier : List Bool × List Bool → Bool} (machine : VerifierTM verifier) (preparation : BitTM (totalVerifierSortedFiveFamilyFlatFoldInput bound machine)) : BitTM (CLStructuralWholeCNFOutputTM.structuralWholeCNFWord bound machine)

GapCVP reduction support.

Equations

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

def GapCVP.CNFFlatSourceOrderPolynomialBounds.tableauSignedLiteralCodeBound (time symbols : ℕ) : ℕ

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceOrderPolynomialBounds.tableauSignedLiteralCodeBound time symbols = (GapCVP.CLStructuralCNFVariableBounds.tableauFiniteVariableCodeBound time symbols + 2) ^ 2

theorem GapCVP.CNFFlatSourceOrderPolynomialBounds.flatSourceClauseLiteralCode_lt {time symbols : ℕ} (clause : CL.Clause time symbols) (code : ℕ) (hcode : code ∈ CNFFlatSourceOrder.flatSourceFinsetCodes clause) : code < tableauSignedLiteralCodeBound time symbols

def GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorWord (polynomial : Polynomial ℕ) (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.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorComputable (polynomial : Polynomial ℕ) (sign : Bool) : BitTM (polynomialSignedLiteralDescriptorWord polynomial sign)

Polynomial-time machine producing a signed, length-prefixed polynomial value.

Equations

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

noncomputable def GapCVP.CNFFlatSourceGridDescriptorTM.tableauSourceSignedLiteralDescriptorWord (sign : Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceGridDescriptorTM.tableauSourceSignedLiteralDescriptorWord sign = GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorWord (4 * Polynomial.X) sign

noncomputable def GapCVP.CNFFlatSourceGridDescriptorTM.tableauSourceSignedLiteralDescriptorComputable (sign : Bool) : BitTM (tableauSourceSignedLiteralDescriptorWord sign)

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceGridDescriptorTM.tableauSourceSignedLiteralDescriptorComputable sign = GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorComputable (4 * Polynomial.X) sign

@[simp]

theorem GapCVP.CNFFlatSourceGridDescriptorTM.tableauSourceSignedLiteralDescriptorWord_variable {T S : ℕ} (sourceVar : CL.Variable T S) (sign : Bool) : tableauSourceSignedLiteralDescriptorWord sign (List.replicate (Encodable.encode sourceVar) true) = CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (ThreeCNFReduction.sourceVariable sourceVar, sign)

noncomputable def GapCVP.CNFFlatSourceGridDescriptorTM.accumulatorSignedLiteralDescriptorWord (sign : Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceGridDescriptorTM.accumulatorSignedLiteralDescriptorWord sign = GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorWord (4 * Polynomial.X + 1) sign

noncomputable def GapCVP.CNFFlatSourceGridDescriptorTM.accumulatorSignedLiteralDescriptorComputable (sign : Bool) : BitTM (accumulatorSignedLiteralDescriptorWord sign)

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceGridDescriptorTM.accumulatorSignedLiteralDescriptorComputable sign = GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorComputable (4 * Polynomial.X + 1) sign

@[simp]

theorem GapCVP.CNFFlatSourceGridDescriptorTM.accumulatorSignedLiteralDescriptorWord_index (clauseIndex prefixIndex : ℕ) (sign : Bool) : accumulatorSignedLiteralDescriptorWord sign (List.replicate (Nat.pair clauseIndex prefixIndex) true) = CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (ThreeCNFReduction.accumulatorVariable clauseIndex prefixIndex, sign)

noncomputable def GapCVP.CNFFlatSourceGridDescriptorTM.paddingSignedLiteralDescriptorWord (index : ℕ) (sign : Bool) : List Bool → List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceGridDescriptorTM.paddingSignedLiteralDescriptorWord index sign = GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorWord (Polynomial.C index) sign

noncomputable def GapCVP.CNFFlatSourceGridDescriptorTM.paddingSignedLiteralDescriptorComputable (index : ℕ) (sign : Bool) : BitTM (paddingSignedLiteralDescriptorWord index sign)

GapCVP reduction support.

Equations

• GapCVP.CNFFlatSourceGridDescriptorTM.paddingSignedLiteralDescriptorComputable index sign = GapCVP.CNFFlatSourceGridDescriptorTM.polynomialSignedLiteralDescriptorComputable (Polynomial.C index) sign

@[simp]

theorem GapCVP.CNFFlatSourceGridDescriptorTM.paddingSignedLiteralDescriptorWord_eq (index : ℕ) (sign : Bool) (input : List Bool) : paddingSignedLiteralDescriptorWord index sign input = CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (index, sign)

def GapCVP.CNFUnaryPairIndexTM.unarySourcePairWord (first second : ℕ) : List Bool

GapCVP reduction support.

Equations

• GapCVP.CNFUnaryPairIndexTM.unarySourcePairWord first second = List.replicate first true ++ false :: (List.replicate second true ++ [false])

def GapCVP.CNFUnaryPairIndexTM.unarySourcePairOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFUnaryPairIndexTM.unarySourcePairOutput_word (first second : ℕ) : unarySourcePairOutput (unarySourcePairWord first second) = List.replicate (Nat.pair first second) true

def GapCVP.CNFUnaryPairIndexTM.unaryPairPeek (stack : Fin 9) (present absent : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

Inspects a unary-pair stack and branches on whether it contains a bit.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairPop (stack : Fin 9) (continuation : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

Removes the top bit of a unary-pair stack and continues.

Equations

• GapCVP.CNFUnaryPairIndexTM.unaryPairPop stack continuation = Turing.TM2.Stmt.pop stack (fun (symbol x : Option Bool) => symbol) continuation

def GapCVP.CNFUnaryPairIndexTM.unaryPairPush (stack : Fin 9) (continuation : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)) : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

Pushes a unary marker onto the selected stack.

Equations

• GapCVP.CNFUnaryPairIndexTM.unaryPairPush stack continuation = Turing.TM2.Stmt.push stack (fun (x : Option Bool) => true) continuation

def GapCVP.CNFUnaryPairIndexTM.unaryPairGoto (phase : Fin 12) : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

Clears the inspected bit and enters the selected unary-pair phase.

Equations

• GapCVP.CNFUnaryPairIndexTM.unaryPairGoto phase = Turing.TM2.Stmt.load (fun (x : Option Bool) => none) (Turing.TM2.Stmt.goto fun (x : Option Bool) => phase)

def GapCVP.CNFUnaryPairIndexTM.unaryPairFirstStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairSecondStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairCompareStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairGreaterBaseStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairGreaterOffsetStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairLessBaseStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairLessOffsetStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairOuterStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairSquareCopyStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairSquareRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairSquareCleanupStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairFailureStatement : Turing.TM2.Stmt (fun (x : Fin 9) => Bool) (Fin 12) (Option Bool)

GapCVP reduction support.

Equations

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

@[reducible, inline]

abbrev GapCVP.CNFUnaryPairIndexTM.actualUnaryPairIndexMachine : Turing.FinTM2

GapCVP reduction support.

Equations

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

def GapCVP.CNFUnaryPairIndexTM.unaryPairConfiguration (phase : Fin 12) (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.Cfg

GapCVP reduction support.

Equations

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

theorem GapCVP.CNFUnaryPairIndexTM.actualUnaryPairIndexMachine_init (input : List Bool) : Turing.initList actualUnaryPairIndexMachine input = unaryPairConfiguration 0 input [] [] [] [] [] [] [] []

def GapCVP.CNFUnaryPairIndexTM.tacticUnaryPairStepTac : Lean.ParserDescr

Executes the unaryPairStepTac machine-step simplifier.

Equations

• GapCVP.CNFUnaryPairIndexTM.tacticUnaryPairStepTac = Lean.ParserDescr.node `GapCVP.CNFUnaryPairIndexTM.tacticUnaryPairStepTac 1024 (Lean.ParserDescr.nonReservedSymbol "unaryPairStepTac" false)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_first_true (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 0 (true :: input) first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 0 input (true :: first) second matchedFirst matchedSecond base outer output scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_first_false (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 0 (false :: input) first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 1 input first second matchedFirst matchedSecond base outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_first_missing (first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 0 [] first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 11 [] first second matchedFirst matchedSecond base outer output scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_second_true (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 1 (true :: input) first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 1 input first (true :: second) matchedFirst matchedSecond base outer output scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_second_false (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 1 (false :: input) first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 2 input first second matchedFirst matchedSecond base outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_second_missing (first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 1 [] first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 11 [] first second matchedFirst matchedSecond base outer output scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_compare_match (first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 2 [] (true :: first) (true :: second) matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 2 [] first second (true :: matchedFirst) (true :: matchedSecond) base outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_compare_greater (first matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 2 [] first [] matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 3 [] first [] matchedFirst matchedSecond base outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_compare_less (second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 2 [] [] (true :: second) matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 5 [] [] (true :: second) matchedFirst matchedSecond base outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_compare_trailing (bit : Bool) (input first second matchedFirst matchedSecond base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 2 (bit :: input) first second matchedFirst matchedSecond base outer output scratch) = some (unaryPairConfiguration 11 (bit :: input) first second matchedFirst matchedSecond base outer output scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_greater_base_first (first matchedFirst matchedSecond base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 3 [] (true :: first) [] matchedFirst matchedSecond base outer output []) = some (unaryPairConfiguration 3 [] first [] matchedFirst matchedSecond (true :: base) (true :: outer) (true :: output) [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_greater_base_matched (matchedFirst matchedSecond base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 3 [] [] [] (true :: matchedFirst) matchedSecond base outer output []) = some (unaryPairConfiguration 3 [] [] [] matchedFirst matchedSecond (true :: base) (true :: outer) (true :: output) [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_greater_base_finish (matchedSecond base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 3 [] [] [] [] matchedSecond base outer output []) = some (unaryPairConfiguration 4 [] [] [] [] matchedSecond base outer output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_greater_offset_step (matchedSecond base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 4 [] [] [] [] (true :: matchedSecond) base outer output []) = some (unaryPairConfiguration 4 [] [] [] [] matchedSecond base outer (true :: output) [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_greater_offset_finish (base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 4 [] [] [] [] [] base outer output []) = some (unaryPairConfiguration 7 [] [] [] [] [] base outer output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_less_base_second (second matchedFirst matchedSecond base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 5 [] [] (true :: second) matchedFirst matchedSecond base outer output []) = some (unaryPairConfiguration 5 [] [] second matchedFirst matchedSecond (true :: base) (true :: outer) output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_less_base_matched (matchedFirst matchedSecond base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 5 [] [] [] matchedFirst (true :: matchedSecond) base outer output []) = some (unaryPairConfiguration 5 [] [] [] matchedFirst matchedSecond (true :: base) (true :: outer) output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_less_base_finish (matchedFirst base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 5 [] [] [] matchedFirst [] base outer output []) = some (unaryPairConfiguration 6 [] [] [] matchedFirst [] base outer output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_less_offset_step (matchedFirst base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 6 [] [] [] (true :: matchedFirst) [] base outer output []) = some (unaryPairConfiguration 6 [] [] [] matchedFirst [] base outer (true :: output) [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_less_offset_finish (base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 6 [] [] [] [] [] base outer output []) = some (unaryPairConfiguration 7 [] [] [] [] [] base outer output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_outer_step (base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 7 [] [] [] [] [] base (true :: outer) output []) = some (unaryPairConfiguration 8 [] [] [] [] [] base outer output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_outer_finish (base output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 7 [] [] [] [] [] base [] output []) = some (unaryPairConfiguration 10 [] [] [] [] [] base [] output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_square_copy_step (base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 8 [] [] [] [] [] (true :: base) outer output scratch) = some (unaryPairConfiguration 8 [] [] [] [] [] base outer (true :: output) (true :: scratch))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_square_copy_finish (outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 8 [] [] [] [] [] [] outer output scratch) = some (unaryPairConfiguration 9 [] [] [] [] [] [] outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_square_restore_step (base outer output scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 9 [] [] [] [] [] base outer output (true :: scratch)) = some (unaryPairConfiguration 9 [] [] [] [] [] (true :: base) outer output scratch)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_square_restore_finish (base outer output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 9 [] [] [] [] [] base outer output []) = some (unaryPairConfiguration 7 [] [] [] [] [] base outer output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_square_cleanup_step (base output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 10 [] [] [] [] [] (true :: base) [] output []) = some (unaryPairConfiguration 10 [] [] [] [] [] base [] output [])

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_square_cleanup_finish (output : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 10 [] [] [] [] [] [] [] output []) = some (Turing.haltList actualUnaryPairIndexMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_input_step (bit : Bool) (input first second matchedFirst matchedSecond base outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 (bit :: input) first second matchedFirst matchedSecond base outer [] scratch) = some (unaryPairConfiguration 11 input first second matchedFirst matchedSecond base outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_first_step (bit : Bool) (first second matchedFirst matchedSecond base outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] (bit :: first) second matchedFirst matchedSecond base outer [] scratch) = some (unaryPairConfiguration 11 [] first second matchedFirst matchedSecond base outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_second_step (bit : Bool) (second matchedFirst matchedSecond base outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] (bit :: second) matchedFirst matchedSecond base outer [] scratch) = some (unaryPairConfiguration 11 [] [] second matchedFirst matchedSecond base outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_matchedFirst_step (bit : Bool) (matchedFirst matchedSecond base outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] (bit :: matchedFirst) matchedSecond base outer [] scratch) = some (unaryPairConfiguration 11 [] [] [] matchedFirst matchedSecond base outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_matchedSecond_step (bit : Bool) (matchedSecond base outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] [] (bit :: matchedSecond) base outer [] scratch) = some (unaryPairConfiguration 11 [] [] [] [] matchedSecond base outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_base_step (bit : Bool) (base outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] [] [] (bit :: base) outer [] scratch) = some (unaryPairConfiguration 11 [] [] [] [] [] base outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_outer_step (bit : Bool) (outer scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] [] [] [] (bit :: outer) [] scratch) = some (unaryPairConfiguration 11 [] [] [] [] [] [] outer [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_scratch_step (bit : Bool) (scratch : List Bool) : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] [] [] [] [] [] (bit :: scratch)) = some (unaryPairConfiguration 11 [] [] [] [] [] [] [] [] scratch)

theorem GapCVP.CNFUnaryPairIndexTM.unaryPair_failure_finish : actualUnaryPairIndexMachine.step (unaryPairConfiguration 11 [] [] [] [] [] [] [] [] []) = some (Turing.haltList actualUnaryPairIndexMachine [])

theorem GapCVP.CNFUnaryPairIndexTotalCert.unaryPair_replicate_append_true (count : ℕ) (suffix : List Bool) : List.replicate count true ++ true :: suffix = List.replicate (count + 1) true ++ suffix