GapCVP proof, part 05

noncomputable def GapCVP.CNFUnaryPairIndexTotalRuntimeCert.actualUnaryPairIndexComputable : BitTM CNFUnaryPairIndexTM.unarySourcePairOutput

GapCVP reduction support.

Equations

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

noncomputable def GapCVP.CNFPairedSourceGridDescriptorTM.pairedAccumulatorSignedLiteralDescriptorWord (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.CNFPairedSourceGridDescriptorTM.pairedAccumulatorSignedLiteralDescriptorComputable (sign : Bool) : BitTM (pairedAccumulatorSignedLiteralDescriptorWord sign)

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFPairedSourceGridDescriptorTM.pairedAccumulatorSignedLiteralDescriptorWord_pair (clauseIndex prefixIndex : ℕ) (sign : Bool) : pairedAccumulatorSignedLiteralDescriptorWord sign (CNFUnaryPairIndexTM.unarySourcePairWord clauseIndex prefixIndex) = CNFFlatStructuralRecordWorkerTM.flatSignedLiteralDescriptor (ThreeCNFReduction.accumulatorVariable clauseIndex prefixIndex, sign)

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixOutput (input : List Bool) : List Bool

GapCVP reduction support.

Equations

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

@[simp]

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixOutput_pair (first second : ℕ) (suffix : List Bool) : sourcePairPrefixOutput (CNFUnaryPairIndexTM.unarySourcePairWord first second ++ suffix) = CNFUnaryPairIndexTM.unarySourcePairWord first second

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixFirstStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixSecondStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixSuffixStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixSecondRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixFirstRestoreStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (Option Bool)

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixFailureStatement : Turing.TM2.Stmt (fun (x : Fin 4) => Bool) (Fin 6) (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.CNFSourcePairPrefixWorkerTM.actualSourcePairPrefixMachine : Turing.FinTM2

Internal support shared across GapCVP continuation modules.

Equations

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

def GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixConfiguration (phase : Fin 6) (input first second output : List Bool) : actualSourcePairPrefixMachine.Cfg

Internal support shared across GapCVP continuation modules.

Equations

• GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefixConfiguration phase input first second output = { l := some phase, var := none, stk := ![input, first, second, output] }

theorem GapCVP.CNFSourcePairPrefixWorkerTM.actualSourcePairPrefixMachine_init (input : List Bool) : Turing.initList actualSourcePairPrefixMachine input = sourcePairPrefixConfiguration 0 input [] [] []

Internal support shared across GapCVP continuation modules.

def GapCVP.CNFSourcePairPrefixWorkerTM.tacticSourcePairPrefixStepTac : Lean.ParserDescr

Executes the sourcePairPrefixStepTac machine-step simplifier.

Equations

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

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_first_true (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 (true :: input) first second output) = some (sourcePairPrefixConfiguration 0 input (true :: first) second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_first_false (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 (false :: input) first second output) = some (sourcePairPrefixConfiguration 1 input first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_first_missing (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 0 [] first second output) = some (sourcePairPrefixConfiguration 5 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_second_true (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 (true :: input) first second output) = some (sourcePairPrefixConfiguration 1 input first (true :: second) output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_second_false (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 (false :: input) first second output) = some (sourcePairPrefixConfiguration 2 input first second (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_second_missing (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 1 [] first second output) = some (sourcePairPrefixConfiguration 5 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_suffix_step (bit : Bool) (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 2 (bit :: input) first second output) = some (sourcePairPrefixConfiguration 2 input first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_suffix_finish (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 2 [] first second output) = some (sourcePairPrefixConfiguration 3 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_secondRestore_step (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 3 [] first (true :: second) output) = some (sourcePairPrefixConfiguration 3 [] first second (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_secondRestore_finish (first output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 3 [] first [] output) = some (sourcePairPrefixConfiguration 4 [] first [] (false :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_firstRestore_step (first output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 4 [] (true :: first) [] output) = some (sourcePairPrefixConfiguration 4 [] first [] (true :: output))

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_firstRestore_finish (output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 4 [] [] [] output) = some (Turing.haltList actualSourcePairPrefixMachine output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_input_step (bit : Bool) (input first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 (bit :: input) first second output) = some (sourcePairPrefixConfiguration 5 input first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_first_step (bit : Bool) (first second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] (bit :: first) second output) = some (sourcePairPrefixConfiguration 5 [] first second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_second_step (bit : Bool) (second output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] (bit :: second) output) = some (sourcePairPrefixConfiguration 5 [] [] second output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_output_step (bit : Bool) (output : List Bool) : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] [] (bit :: output)) = some (sourcePairPrefixConfiguration 5 [] [] [] output)

Internal support shared across GapCVP continuation modules.

theorem GapCVP.CNFSourcePairPrefixWorkerTM.sourcePairPrefix_failure_finish : actualSourcePairPrefixMachine.step (sourcePairPrefixConfiguration 5 [] [] [] []) = some (Turing.haltList actualSourcePairPrefixMachine [])

Internal support shared across GapCVP continuation modules.