GapCVP proof, part 04, continuation 06

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.

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.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

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

@[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

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

@[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.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